Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ismrcd1 Structured version   Visualization version   GIF version

Theorem ismrcd1 37578
Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 16324), isotone (satisfies mrcss 16323), and idempotent (satisfies mrcidm 16326) has a collection of fixed points which is a Moore collection, and itself is the closure operator for that collection. This can be taken as an alternate definition for the closure operators. This is the first half, ismrcd2 37579 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Hypotheses
Ref Expression
ismrcd.b (𝜑𝐵𝑉)
ismrcd.f (𝜑𝐹:𝒫 𝐵⟶𝒫 𝐵)
ismrcd.e ((𝜑𝑥𝐵) → 𝑥 ⊆ (𝐹𝑥))
ismrcd.m ((𝜑𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥))
ismrcd.i ((𝜑𝑥𝐵) → (𝐹‘(𝐹𝑥)) = (𝐹𝑥))
Assertion
Ref Expression
ismrcd1 (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))
Distinct variable groups:   𝜑,𝑥,𝑦   𝑥,𝐵,𝑦   𝑥,𝐹,𝑦   𝑥,𝑉,𝑦

Proof of Theorem ismrcd1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 inss1 3866 . . . 4 (𝐹 ∩ I ) ⊆ 𝐹
2 dmss 5355 . . . 4 ((𝐹 ∩ I ) ⊆ 𝐹 → dom (𝐹 ∩ I ) ⊆ dom 𝐹)
31, 2ax-mp 5 . . 3 dom (𝐹 ∩ I ) ⊆ dom 𝐹
4 ismrcd.f . . . 4 (𝜑𝐹:𝒫 𝐵⟶𝒫 𝐵)
5 fdm 6089 . . . 4 (𝐹:𝒫 𝐵⟶𝒫 𝐵 → dom 𝐹 = 𝒫 𝐵)
64, 5syl 17 . . 3 (𝜑 → dom 𝐹 = 𝒫 𝐵)
73, 6syl5sseq 3686 . 2 (𝜑 → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
8 ssid 3657 . . . . . . 7 𝐵𝐵
9 ismrcd.b . . . . . . . 8 (𝜑𝐵𝑉)
10 elpwg 4199 . . . . . . . 8 (𝐵𝑉 → (𝐵 ∈ 𝒫 𝐵𝐵𝐵))
119, 10syl 17 . . . . . . 7 (𝜑 → (𝐵 ∈ 𝒫 𝐵𝐵𝐵))
128, 11mpbiri 248 . . . . . 6 (𝜑𝐵 ∈ 𝒫 𝐵)
134, 12ffvelrnd 6400 . . . . 5 (𝜑 → (𝐹𝐵) ∈ 𝒫 𝐵)
1413elpwid 4203 . . . 4 (𝜑 → (𝐹𝐵) ⊆ 𝐵)
15 selpw 4198 . . . . . . 7 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
16 ismrcd.e . . . . . . 7 ((𝜑𝑥𝐵) → 𝑥 ⊆ (𝐹𝑥))
1715, 16sylan2b 491 . . . . . 6 ((𝜑𝑥 ∈ 𝒫 𝐵) → 𝑥 ⊆ (𝐹𝑥))
1817ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥))
19 id 22 . . . . . . 7 (𝑥 = 𝐵𝑥 = 𝐵)
20 fveq2 6229 . . . . . . 7 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
2119, 20sseq12d 3667 . . . . . 6 (𝑥 = 𝐵 → (𝑥 ⊆ (𝐹𝑥) ↔ 𝐵 ⊆ (𝐹𝐵)))
2221rspcva 3338 . . . . 5 ((𝐵 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥)) → 𝐵 ⊆ (𝐹𝐵))
2312, 18, 22syl2anc 694 . . . 4 (𝜑𝐵 ⊆ (𝐹𝐵))
2414, 23eqssd 3653 . . 3 (𝜑 → (𝐹𝐵) = 𝐵)
25 ffn 6083 . . . . 5 (𝐹:𝒫 𝐵⟶𝒫 𝐵𝐹 Fn 𝒫 𝐵)
264, 25syl 17 . . . 4 (𝜑𝐹 Fn 𝒫 𝐵)
27 fnelfp 6482 . . . 4 ((𝐹 Fn 𝒫 𝐵𝐵 ∈ 𝒫 𝐵) → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝐵) = 𝐵))
2826, 12, 27syl2anc 694 . . 3 (𝜑 → (𝐵 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝐵) = 𝐵))
2924, 28mpbird 247 . 2 (𝜑𝐵 ∈ dom (𝐹 ∩ I ))
30 simp2 1082 . . . . . . . . . . . . 13 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ dom (𝐹 ∩ I ))
3173ad2ant1 1102 . . . . . . . . . . . . 13 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → dom (𝐹 ∩ I ) ⊆ 𝒫 𝐵)
3230, 31sstrd 3646 . . . . . . . . . . . 12 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ 𝒫 𝐵)
33 simp3 1083 . . . . . . . . . . . 12 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ≠ ∅)
34 intssuni2 4534 . . . . . . . . . . . 12 ((𝑧 ⊆ 𝒫 𝐵𝑧 ≠ ∅) → 𝑧 𝒫 𝐵)
3532, 33, 34syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 𝒫 𝐵)
36 unipw 4948 . . . . . . . . . . 11 𝒫 𝐵 = 𝐵
3735, 36syl6sseq 3684 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧𝐵)
38 intex 4850 . . . . . . . . . . . 12 (𝑧 ≠ ∅ ↔ 𝑧 ∈ V)
39 elpwg 4199 . . . . . . . . . . . 12 ( 𝑧 ∈ V → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
4038, 39sylbi 207 . . . . . . . . . . 11 (𝑧 ≠ ∅ → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
41403ad2ant3 1104 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ( 𝑧 ∈ 𝒫 𝐵 𝑧𝐵))
4237, 41mpbird 247 . . . . . . . . 9 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝒫 𝐵)
4342adantr 480 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑧 ∈ 𝒫 𝐵)
44 ismrcd.m . . . . . . . . . . . 12 ((𝜑𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥))
45443expib 1287 . . . . . . . . . . 11 (𝜑 → ((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4645alrimiv 1895 . . . . . . . . . 10 (𝜑 → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
47463ad2ant1 1102 . . . . . . . . 9 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4847adantr 480 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → ∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)))
4932sselda 3636 . . . . . . . . . 10 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥 ∈ 𝒫 𝐵)
5049elpwid 4203 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥𝐵)
51 intss1 4524 . . . . . . . . . 10 (𝑥𝑧 𝑧𝑥)
5251adantl 481 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑧𝑥)
5350, 52jca 553 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝑥𝐵 𝑧𝑥))
54 sseq1 3659 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦𝑥 𝑧𝑥))
5554anbi2d 740 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝑥𝐵𝑦𝑥) ↔ (𝑥𝐵 𝑧𝑥)))
56 fveq2 6229 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹 𝑧))
5756sseq1d 3665 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝐹𝑦) ⊆ (𝐹𝑥) ↔ (𝐹 𝑧) ⊆ (𝐹𝑥)))
5855, 57imbi12d 333 . . . . . . . . 9 (𝑦 = 𝑧 → (((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)) ↔ ((𝑥𝐵 𝑧𝑥) → (𝐹 𝑧) ⊆ (𝐹𝑥))))
5958spcgv 3324 . . . . . . . 8 ( 𝑧 ∈ 𝒫 𝐵 → (∀𝑦((𝑥𝐵𝑦𝑥) → (𝐹𝑦) ⊆ (𝐹𝑥)) → ((𝑥𝐵 𝑧𝑥) → (𝐹 𝑧) ⊆ (𝐹𝑥))))
6043, 48, 53, 59syl3c 66 . . . . . . 7 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹 𝑧) ⊆ (𝐹𝑥))
6130sselda 3636 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝑥 ∈ dom (𝐹 ∩ I ))
62263ad2ant1 1102 . . . . . . . . . 10 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝐹 Fn 𝒫 𝐵)
6362adantr 480 . . . . . . . . 9 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → 𝐹 Fn 𝒫 𝐵)
64 fnelfp 6482 . . . . . . . . 9 ((𝐹 Fn 𝒫 𝐵𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝑥) = 𝑥))
6563, 49, 64syl2anc 694 . . . . . . . 8 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝑥 ∈ dom (𝐹 ∩ I ) ↔ (𝐹𝑥) = 𝑥))
6661, 65mpbid 222 . . . . . . 7 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹𝑥) = 𝑥)
6760, 66sseqtrd 3674 . . . . . 6 (((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) ∧ 𝑥𝑧) → (𝐹 𝑧) ⊆ 𝑥)
6867ralrimiva 2995 . . . . 5 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥𝑧 (𝐹 𝑧) ⊆ 𝑥)
69 ssint 4525 . . . . 5 ((𝐹 𝑧) ⊆ 𝑧 ↔ ∀𝑥𝑧 (𝐹 𝑧) ⊆ 𝑥)
7068, 69sylibr 224 . . . 4 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹 𝑧) ⊆ 𝑧)
71183ad2ant1 1102 . . . . 5 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥))
72 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
73 fveq2 6229 . . . . . . 7 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹 𝑧))
7472, 73sseq12d 3667 . . . . . 6 (𝑥 = 𝑧 → (𝑥 ⊆ (𝐹𝑥) ↔ 𝑧 ⊆ (𝐹 𝑧)))
7574rspcva 3338 . . . . 5 (( 𝑧 ∈ 𝒫 𝐵 ∧ ∀𝑥 ∈ 𝒫 𝐵𝑥 ⊆ (𝐹𝑥)) → 𝑧 ⊆ (𝐹 𝑧))
7642, 71, 75syl2anc 694 . . . 4 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ⊆ (𝐹 𝑧))
7770, 76eqssd 3653 . . 3 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → (𝐹 𝑧) = 𝑧)
78 fnelfp 6482 . . . 4 ((𝐹 Fn 𝒫 𝐵 𝑧 ∈ 𝒫 𝐵) → ( 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹 𝑧) = 𝑧))
7962, 42, 78syl2anc 694 . . 3 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → ( 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (𝐹 𝑧) = 𝑧))
8077, 79mpbird 247 . 2 ((𝜑𝑧 ⊆ dom (𝐹 ∩ I ) ∧ 𝑧 ≠ ∅) → 𝑧 ∈ dom (𝐹 ∩ I ))
817, 29, 80ismred 16309 1 (𝜑 → dom (𝐹 ∩ I ) ∈ (Moore‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054  wal 1521   = wceq 1523  wcel 2030  wne 2823  wral 2941  Vcvv 3231  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191   cuni 4468   cint 4507   I cid 5052  dom cdm 5143   Fn wfn 5921  wf 5922  cfv 5926  Moorecmre 16289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-int 4508  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-mre 16293
This theorem is referenced by:  ismrcd2  37579  istopclsd  37580  ismrc  37581
  Copyright terms: Public domain W3C validator