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 41738
Description: Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17565), isotone (satisfies mrcss 17564), and idempotent (satisfies mrcidm 17567) 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 41739 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 4228 . . . 4 (𝐹 ∩ I ) βŠ† 𝐹
2 dmss 5902 . . . 4 ((𝐹 ∩ I ) βŠ† 𝐹 β†’ dom (𝐹 ∩ I ) βŠ† dom 𝐹)
31, 2ax-mp 5 . . 3 dom (𝐹 ∩ I ) βŠ† dom 𝐹
4 ismrcd.f . . 3 (πœ‘ β†’ 𝐹:𝒫 π΅βŸΆπ’« 𝐡)
53, 4fssdm 6737 . 2 (πœ‘ β†’ dom (𝐹 ∩ I ) βŠ† 𝒫 𝐡)
6 ssid 4004 . . . . . . 7 𝐡 βŠ† 𝐡
7 ismrcd.b . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ 𝑉)
8 elpwg 4605 . . . . . . . 8 (𝐡 ∈ 𝑉 β†’ (𝐡 ∈ 𝒫 𝐡 ↔ 𝐡 βŠ† 𝐡))
97, 8syl 17 . . . . . . 7 (πœ‘ β†’ (𝐡 ∈ 𝒫 𝐡 ↔ 𝐡 βŠ† 𝐡))
106, 9mpbiri 257 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ 𝒫 𝐡)
114, 10ffvelcdmd 7087 . . . . 5 (πœ‘ β†’ (πΉβ€˜π΅) ∈ 𝒫 𝐡)
1211elpwid 4611 . . . 4 (πœ‘ β†’ (πΉβ€˜π΅) βŠ† 𝐡)
13 velpw 4607 . . . . . . 7 (π‘₯ ∈ 𝒫 𝐡 ↔ π‘₯ βŠ† 𝐡)
14 ismrcd.e . . . . . . 7 ((πœ‘ ∧ π‘₯ βŠ† 𝐡) β†’ π‘₯ βŠ† (πΉβ€˜π‘₯))
1513, 14sylan2b 594 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝒫 𝐡) β†’ π‘₯ βŠ† (πΉβ€˜π‘₯))
1615ralrimiva 3146 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝒫 𝐡π‘₯ βŠ† (πΉβ€˜π‘₯))
17 id 22 . . . . . . 7 (π‘₯ = 𝐡 β†’ π‘₯ = 𝐡)
18 fveq2 6891 . . . . . . 7 (π‘₯ = 𝐡 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π΅))
1917, 18sseq12d 4015 . . . . . 6 (π‘₯ = 𝐡 β†’ (π‘₯ βŠ† (πΉβ€˜π‘₯) ↔ 𝐡 βŠ† (πΉβ€˜π΅)))
2019rspcva 3610 . . . . 5 ((𝐡 ∈ 𝒫 𝐡 ∧ βˆ€π‘₯ ∈ 𝒫 𝐡π‘₯ βŠ† (πΉβ€˜π‘₯)) β†’ 𝐡 βŠ† (πΉβ€˜π΅))
2110, 16, 20syl2anc 584 . . . 4 (πœ‘ β†’ 𝐡 βŠ† (πΉβ€˜π΅))
2212, 21eqssd 3999 . . 3 (πœ‘ β†’ (πΉβ€˜π΅) = 𝐡)
234ffnd 6718 . . . 4 (πœ‘ β†’ 𝐹 Fn 𝒫 𝐡)
24 fnelfp 7175 . . . 4 ((𝐹 Fn 𝒫 𝐡 ∧ 𝐡 ∈ 𝒫 𝐡) β†’ (𝐡 ∈ dom (𝐹 ∩ I ) ↔ (πΉβ€˜π΅) = 𝐡))
2523, 10, 24syl2anc 584 . . 3 (πœ‘ β†’ (𝐡 ∈ dom (𝐹 ∩ I ) ↔ (πΉβ€˜π΅) = 𝐡))
2622, 25mpbird 256 . 2 (πœ‘ β†’ 𝐡 ∈ dom (𝐹 ∩ I ))
27 simp2 1137 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ 𝑧 βŠ† dom (𝐹 ∩ I ))
2853ad2ant1 1133 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ dom (𝐹 ∩ I ) βŠ† 𝒫 𝐡)
2927, 28sstrd 3992 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ 𝑧 βŠ† 𝒫 𝐡)
30 simp3 1138 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ 𝑧 β‰  βˆ…)
31 intssuni2 4977 . . . . . . . . . . . 12 ((𝑧 βŠ† 𝒫 𝐡 ∧ 𝑧 β‰  βˆ…) β†’ ∩ 𝑧 βŠ† βˆͺ 𝒫 𝐡)
3229, 30, 31syl2anc 584 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ ∩ 𝑧 βŠ† βˆͺ 𝒫 𝐡)
33 unipw 5450 . . . . . . . . . . 11 βˆͺ 𝒫 𝐡 = 𝐡
3432, 33sseqtrdi 4032 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ ∩ 𝑧 βŠ† 𝐡)
35 intex 5337 . . . . . . . . . . . 12 (𝑧 β‰  βˆ… ↔ ∩ 𝑧 ∈ V)
36 elpwg 4605 . . . . . . . . . . . 12 (∩ 𝑧 ∈ V β†’ (∩ 𝑧 ∈ 𝒫 𝐡 ↔ ∩ 𝑧 βŠ† 𝐡))
3735, 36sylbi 216 . . . . . . . . . . 11 (𝑧 β‰  βˆ… β†’ (∩ 𝑧 ∈ 𝒫 𝐡 ↔ ∩ 𝑧 βŠ† 𝐡))
38373ad2ant3 1135 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ (∩ 𝑧 ∈ 𝒫 𝐡 ↔ ∩ 𝑧 βŠ† 𝐡))
3934, 38mpbird 256 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ ∩ 𝑧 ∈ 𝒫 𝐡)
4039adantr 481 . . . . . . . 8 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ ∩ 𝑧 ∈ 𝒫 𝐡)
41 ismrcd.m . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ βŠ† 𝐡 ∧ 𝑦 βŠ† π‘₯) β†’ (πΉβ€˜π‘¦) βŠ† (πΉβ€˜π‘₯))
42413expib 1122 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘₯ βŠ† 𝐡 ∧ 𝑦 βŠ† π‘₯) β†’ (πΉβ€˜π‘¦) βŠ† (πΉβ€˜π‘₯)))
4342alrimiv 1930 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘¦((π‘₯ βŠ† 𝐡 ∧ 𝑦 βŠ† π‘₯) β†’ (πΉβ€˜π‘¦) βŠ† (πΉβ€˜π‘₯)))
44433ad2ant1 1133 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ βˆ€π‘¦((π‘₯ βŠ† 𝐡 ∧ 𝑦 βŠ† π‘₯) β†’ (πΉβ€˜π‘¦) βŠ† (πΉβ€˜π‘₯)))
4544adantr 481 . . . . . . . 8 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ βˆ€π‘¦((π‘₯ βŠ† 𝐡 ∧ 𝑦 βŠ† π‘₯) β†’ (πΉβ€˜π‘¦) βŠ† (πΉβ€˜π‘₯)))
4629sselda 3982 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ π‘₯ ∈ 𝒫 𝐡)
4746elpwid 4611 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ π‘₯ βŠ† 𝐡)
48 intss1 4967 . . . . . . . . . 10 (π‘₯ ∈ 𝑧 β†’ ∩ 𝑧 βŠ† π‘₯)
4948adantl 482 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ ∩ 𝑧 βŠ† π‘₯)
5047, 49jca 512 . . . . . . . 8 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ (π‘₯ βŠ† 𝐡 ∧ ∩ 𝑧 βŠ† π‘₯))
51 sseq1 4007 . . . . . . . . . . 11 (𝑦 = ∩ 𝑧 β†’ (𝑦 βŠ† π‘₯ ↔ ∩ 𝑧 βŠ† π‘₯))
5251anbi2d 629 . . . . . . . . . 10 (𝑦 = ∩ 𝑧 β†’ ((π‘₯ βŠ† 𝐡 ∧ 𝑦 βŠ† π‘₯) ↔ (π‘₯ βŠ† 𝐡 ∧ ∩ 𝑧 βŠ† π‘₯)))
53 fveq2 6891 . . . . . . . . . . 11 (𝑦 = ∩ 𝑧 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜βˆ© 𝑧))
5453sseq1d 4013 . . . . . . . . . 10 (𝑦 = ∩ 𝑧 β†’ ((πΉβ€˜π‘¦) βŠ† (πΉβ€˜π‘₯) ↔ (πΉβ€˜βˆ© 𝑧) βŠ† (πΉβ€˜π‘₯)))
5552, 54imbi12d 344 . . . . . . . . 9 (𝑦 = ∩ 𝑧 β†’ (((π‘₯ βŠ† 𝐡 ∧ 𝑦 βŠ† π‘₯) β†’ (πΉβ€˜π‘¦) βŠ† (πΉβ€˜π‘₯)) ↔ ((π‘₯ βŠ† 𝐡 ∧ ∩ 𝑧 βŠ† π‘₯) β†’ (πΉβ€˜βˆ© 𝑧) βŠ† (πΉβ€˜π‘₯))))
5655spcgv 3586 . . . . . . . 8 (∩ 𝑧 ∈ 𝒫 𝐡 β†’ (βˆ€π‘¦((π‘₯ βŠ† 𝐡 ∧ 𝑦 βŠ† π‘₯) β†’ (πΉβ€˜π‘¦) βŠ† (πΉβ€˜π‘₯)) β†’ ((π‘₯ βŠ† 𝐡 ∧ ∩ 𝑧 βŠ† π‘₯) β†’ (πΉβ€˜βˆ© 𝑧) βŠ† (πΉβ€˜π‘₯))))
5740, 45, 50, 56syl3c 66 . . . . . . 7 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ (πΉβ€˜βˆ© 𝑧) βŠ† (πΉβ€˜π‘₯))
5827sselda 3982 . . . . . . . 8 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ π‘₯ ∈ dom (𝐹 ∩ I ))
59233ad2ant1 1133 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ 𝐹 Fn 𝒫 𝐡)
6059adantr 481 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ 𝐹 Fn 𝒫 𝐡)
61 fnelfp 7175 . . . . . . . . 9 ((𝐹 Fn 𝒫 𝐡 ∧ π‘₯ ∈ 𝒫 𝐡) β†’ (π‘₯ ∈ dom (𝐹 ∩ I ) ↔ (πΉβ€˜π‘₯) = π‘₯))
6260, 46, 61syl2anc 584 . . . . . . . 8 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ (π‘₯ ∈ dom (𝐹 ∩ I ) ↔ (πΉβ€˜π‘₯) = π‘₯))
6358, 62mpbid 231 . . . . . . 7 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ (πΉβ€˜π‘₯) = π‘₯)
6457, 63sseqtrd 4022 . . . . . 6 (((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) ∧ π‘₯ ∈ 𝑧) β†’ (πΉβ€˜βˆ© 𝑧) βŠ† π‘₯)
6564ralrimiva 3146 . . . . 5 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ βˆ€π‘₯ ∈ 𝑧 (πΉβ€˜βˆ© 𝑧) βŠ† π‘₯)
66 ssint 4968 . . . . 5 ((πΉβ€˜βˆ© 𝑧) βŠ† ∩ 𝑧 ↔ βˆ€π‘₯ ∈ 𝑧 (πΉβ€˜βˆ© 𝑧) βŠ† π‘₯)
6765, 66sylibr 233 . . . 4 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ (πΉβ€˜βˆ© 𝑧) βŠ† ∩ 𝑧)
68163ad2ant1 1133 . . . . 5 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ βˆ€π‘₯ ∈ 𝒫 𝐡π‘₯ βŠ† (πΉβ€˜π‘₯))
69 id 22 . . . . . . 7 (π‘₯ = ∩ 𝑧 β†’ π‘₯ = ∩ 𝑧)
70 fveq2 6891 . . . . . . 7 (π‘₯ = ∩ 𝑧 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜βˆ© 𝑧))
7169, 70sseq12d 4015 . . . . . 6 (π‘₯ = ∩ 𝑧 β†’ (π‘₯ βŠ† (πΉβ€˜π‘₯) ↔ ∩ 𝑧 βŠ† (πΉβ€˜βˆ© 𝑧)))
7271rspcva 3610 . . . . 5 ((∩ 𝑧 ∈ 𝒫 𝐡 ∧ βˆ€π‘₯ ∈ 𝒫 𝐡π‘₯ βŠ† (πΉβ€˜π‘₯)) β†’ ∩ 𝑧 βŠ† (πΉβ€˜βˆ© 𝑧))
7339, 68, 72syl2anc 584 . . . 4 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ ∩ 𝑧 βŠ† (πΉβ€˜βˆ© 𝑧))
7467, 73eqssd 3999 . . 3 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ (πΉβ€˜βˆ© 𝑧) = ∩ 𝑧)
75 fnelfp 7175 . . . 4 ((𝐹 Fn 𝒫 𝐡 ∧ ∩ 𝑧 ∈ 𝒫 𝐡) β†’ (∩ 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (πΉβ€˜βˆ© 𝑧) = ∩ 𝑧))
7659, 39, 75syl2anc 584 . . 3 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ (∩ 𝑧 ∈ dom (𝐹 ∩ I ) ↔ (πΉβ€˜βˆ© 𝑧) = ∩ 𝑧))
7774, 76mpbird 256 . 2 ((πœ‘ ∧ 𝑧 βŠ† dom (𝐹 ∩ I ) ∧ 𝑧 β‰  βˆ…) β†’ ∩ 𝑧 ∈ dom (𝐹 ∩ I ))
785, 26, 77ismred 17550 1 (πœ‘ β†’ dom (𝐹 ∩ I ) ∈ (Mooreβ€˜π΅))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  βˆ€wal 1539   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  Vcvv 3474   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  βˆͺ cuni 4908  βˆ© cint 4950   I cid 5573  dom cdm 5676   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  Moorecmre 17530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-mre 17534
This theorem is referenced by:  ismrcd2  41739  istopclsd  41740  ismrc  41741
  Copyright terms: Public domain W3C validator