Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mretopd Structured version   Visualization version   GIF version

Theorem mretopd 20819
 Description: A Moore collection which is closed under finite unions called topological; such a collection is the closed sets of a canonically associated topology. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Hypotheses
Ref Expression
mretopd.m (𝜑𝑀 ∈ (Moore‘𝐵))
mretopd.z (𝜑 → ∅ ∈ 𝑀)
mretopd.u ((𝜑𝑥𝑀𝑦𝑀) → (𝑥𝑦) ∈ 𝑀)
mretopd.j 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀}
Assertion
Ref Expression
mretopd (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽)))
Distinct variable groups:   𝜑,𝑥,𝑦,𝑧   𝑥,𝑀,𝑦,𝑧   𝑥,𝐽,𝑦   𝑥,𝐵,𝑦,𝑧
Allowed substitution hint:   𝐽(𝑧)

Proof of Theorem mretopd
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unieq 4415 . . . . . . . . 9 (𝑎 = ∅ → 𝑎 = ∅)
2 uni0 4436 . . . . . . . . 9 ∅ = ∅
31, 2syl6eq 2671 . . . . . . . 8 (𝑎 = ∅ → 𝑎 = ∅)
43eleq1d 2683 . . . . . . 7 (𝑎 = ∅ → ( 𝑎𝐽 ↔ ∅ ∈ 𝐽))
5 mretopd.j . . . . . . . . . . . . . 14 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀}
6 ssrab2 3671 . . . . . . . . . . . . . 14 {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀} ⊆ 𝒫 𝐵
75, 6eqsstri 3619 . . . . . . . . . . . . 13 𝐽 ⊆ 𝒫 𝐵
8 sstr 3595 . . . . . . . . . . . . 13 ((𝑎𝐽𝐽 ⊆ 𝒫 𝐵) → 𝑎 ⊆ 𝒫 𝐵)
97, 8mpan2 706 . . . . . . . . . . . 12 (𝑎𝐽𝑎 ⊆ 𝒫 𝐵)
109adantl 482 . . . . . . . . . . 11 ((𝜑𝑎𝐽) → 𝑎 ⊆ 𝒫 𝐵)
11 sspwuni 4582 . . . . . . . . . . 11 (𝑎 ⊆ 𝒫 𝐵 𝑎𝐵)
1210, 11sylib 208 . . . . . . . . . 10 ((𝜑𝑎𝐽) → 𝑎𝐵)
13 vuniex 6914 . . . . . . . . . . 11 𝑎 ∈ V
1413elpw 4141 . . . . . . . . . 10 ( 𝑎 ∈ 𝒫 𝐵 𝑎𝐵)
1512, 14sylibr 224 . . . . . . . . 9 ((𝜑𝑎𝐽) → 𝑎 ∈ 𝒫 𝐵)
1615adantr 481 . . . . . . . 8 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑎 ∈ 𝒫 𝐵)
17 uniiun 4544 . . . . . . . . . 10 𝑎 = 𝑏𝑎 𝑏
1817difeq2i 3708 . . . . . . . . 9 (𝐵 𝑎) = (𝐵 𝑏𝑎 𝑏)
19 iindif2 4560 . . . . . . . . . . 11 (𝑎 ≠ ∅ → 𝑏𝑎 (𝐵𝑏) = (𝐵 𝑏𝑎 𝑏))
2019adantl 482 . . . . . . . . . 10 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑏𝑎 (𝐵𝑏) = (𝐵 𝑏𝑎 𝑏))
21 mretopd.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ (Moore‘𝐵))
2221ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑀 ∈ (Moore‘𝐵))
23 simpr 477 . . . . . . . . . . 11 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑎 ≠ ∅)
24 difeq2 3705 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑏 → (𝐵𝑧) = (𝐵𝑏))
2524eleq1d 2683 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑏 → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵𝑏) ∈ 𝑀))
2625, 5elrab2 3352 . . . . . . . . . . . . . . 15 (𝑏𝐽 ↔ (𝑏 ∈ 𝒫 𝐵 ∧ (𝐵𝑏) ∈ 𝑀))
2726simprbi 480 . . . . . . . . . . . . . 14 (𝑏𝐽 → (𝐵𝑏) ∈ 𝑀)
2827rgen 2917 . . . . . . . . . . . . 13 𝑏𝐽 (𝐵𝑏) ∈ 𝑀
29 ssralv 3650 . . . . . . . . . . . . . 14 (𝑎𝐽 → (∀𝑏𝐽 (𝐵𝑏) ∈ 𝑀 → ∀𝑏𝑎 (𝐵𝑏) ∈ 𝑀))
3029adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑎𝐽) → (∀𝑏𝐽 (𝐵𝑏) ∈ 𝑀 → ∀𝑏𝑎 (𝐵𝑏) ∈ 𝑀))
3128, 30mpi 20 . . . . . . . . . . . 12 ((𝜑𝑎𝐽) → ∀𝑏𝑎 (𝐵𝑏) ∈ 𝑀)
3231adantr 481 . . . . . . . . . . 11 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → ∀𝑏𝑎 (𝐵𝑏) ∈ 𝑀)
33 mreiincl 16188 . . . . . . . . . . 11 ((𝑀 ∈ (Moore‘𝐵) ∧ 𝑎 ≠ ∅ ∧ ∀𝑏𝑎 (𝐵𝑏) ∈ 𝑀) → 𝑏𝑎 (𝐵𝑏) ∈ 𝑀)
3422, 23, 32, 33syl3anc 1323 . . . . . . . . . 10 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑏𝑎 (𝐵𝑏) ∈ 𝑀)
3520, 34eqeltrrd 2699 . . . . . . . . 9 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 𝑏𝑎 𝑏) ∈ 𝑀)
3618, 35syl5eqel 2702 . . . . . . . 8 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 𝑎) ∈ 𝑀)
37 difeq2 3705 . . . . . . . . . 10 (𝑧 = 𝑎 → (𝐵𝑧) = (𝐵 𝑎))
3837eleq1d 2683 . . . . . . . . 9 (𝑧 = 𝑎 → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵 𝑎) ∈ 𝑀))
3938, 5elrab2 3352 . . . . . . . 8 ( 𝑎𝐽 ↔ ( 𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 𝑎) ∈ 𝑀))
4016, 36, 39sylanbrc 697 . . . . . . 7 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑎𝐽)
41 0elpw 4799 . . . . . . . . . 10 ∅ ∈ 𝒫 𝐵
4241a1i 11 . . . . . . . . 9 (𝜑 → ∅ ∈ 𝒫 𝐵)
43 mre1cl 16186 . . . . . . . . . 10 (𝑀 ∈ (Moore‘𝐵) → 𝐵𝑀)
4421, 43syl 17 . . . . . . . . 9 (𝜑𝐵𝑀)
45 difeq2 3705 . . . . . . . . . . . 12 (𝑧 = ∅ → (𝐵𝑧) = (𝐵 ∖ ∅))
46 dif0 3929 . . . . . . . . . . . 12 (𝐵 ∖ ∅) = 𝐵
4745, 46syl6eq 2671 . . . . . . . . . . 11 (𝑧 = ∅ → (𝐵𝑧) = 𝐵)
4847eleq1d 2683 . . . . . . . . . 10 (𝑧 = ∅ → ((𝐵𝑧) ∈ 𝑀𝐵𝑀))
4948, 5elrab2 3352 . . . . . . . . 9 (∅ ∈ 𝐽 ↔ (∅ ∈ 𝒫 𝐵𝐵𝑀))
5042, 44, 49sylanbrc 697 . . . . . . . 8 (𝜑 → ∅ ∈ 𝐽)
5150adantr 481 . . . . . . 7 ((𝜑𝑎𝐽) → ∅ ∈ 𝐽)
524, 40, 51pm2.61ne 2875 . . . . . 6 ((𝜑𝑎𝐽) → 𝑎𝐽)
5352ex 450 . . . . 5 (𝜑 → (𝑎𝐽 𝑎𝐽))
5453alrimiv 1852 . . . 4 (𝜑 → ∀𝑎(𝑎𝐽 𝑎𝐽))
55 inss1 3816 . . . . . . . 8 (𝑎𝑏) ⊆ 𝑎
56 difeq2 3705 . . . . . . . . . . . . 13 (𝑧 = 𝑎 → (𝐵𝑧) = (𝐵𝑎))
5756eleq1d 2683 . . . . . . . . . . . 12 (𝑧 = 𝑎 → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵𝑎) ∈ 𝑀))
5857, 5elrab2 3352 . . . . . . . . . . 11 (𝑎𝐽 ↔ (𝑎 ∈ 𝒫 𝐵 ∧ (𝐵𝑎) ∈ 𝑀))
5958simplbi 476 . . . . . . . . . 10 (𝑎𝐽𝑎 ∈ 𝒫 𝐵)
6059elpwid 4146 . . . . . . . . 9 (𝑎𝐽𝑎𝐵)
6160ad2antrl 763 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → 𝑎𝐵)
6255, 61syl5ss 3598 . . . . . . 7 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝑎𝑏) ⊆ 𝐵)
63 vex 3192 . . . . . . . . 9 𝑎 ∈ V
6463inex1 4764 . . . . . . . 8 (𝑎𝑏) ∈ V
6564elpw 4141 . . . . . . 7 ((𝑎𝑏) ∈ 𝒫 𝐵 ↔ (𝑎𝑏) ⊆ 𝐵)
6662, 65sylibr 224 . . . . . 6 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝑎𝑏) ∈ 𝒫 𝐵)
67 difindi 3862 . . . . . . 7 (𝐵 ∖ (𝑎𝑏)) = ((𝐵𝑎) ∪ (𝐵𝑏))
6858simprbi 480 . . . . . . . . 9 (𝑎𝐽 → (𝐵𝑎) ∈ 𝑀)
6968ad2antrl 763 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝐵𝑎) ∈ 𝑀)
7027ad2antll 764 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝐵𝑏) ∈ 𝑀)
71 simpl 473 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → 𝜑)
72 uneq1 3743 . . . . . . . . . . . 12 (𝑥 = (𝐵𝑎) → (𝑥𝑦) = ((𝐵𝑎) ∪ 𝑦))
7372eleq1d 2683 . . . . . . . . . . 11 (𝑥 = (𝐵𝑎) → ((𝑥𝑦) ∈ 𝑀 ↔ ((𝐵𝑎) ∪ 𝑦) ∈ 𝑀))
7473imbi2d 330 . . . . . . . . . 10 (𝑥 = (𝐵𝑎) → ((𝜑 → (𝑥𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵𝑎) ∪ 𝑦) ∈ 𝑀)))
75 uneq2 3744 . . . . . . . . . . . 12 (𝑦 = (𝐵𝑏) → ((𝐵𝑎) ∪ 𝑦) = ((𝐵𝑎) ∪ (𝐵𝑏)))
7675eleq1d 2683 . . . . . . . . . . 11 (𝑦 = (𝐵𝑏) → (((𝐵𝑎) ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵𝑎) ∪ (𝐵𝑏)) ∈ 𝑀))
7776imbi2d 330 . . . . . . . . . 10 (𝑦 = (𝐵𝑏) → ((𝜑 → ((𝐵𝑎) ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵𝑎) ∪ (𝐵𝑏)) ∈ 𝑀)))
78 mretopd.u . . . . . . . . . . . 12 ((𝜑𝑥𝑀𝑦𝑀) → (𝑥𝑦) ∈ 𝑀)
79783expb 1263 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑀𝑦𝑀)) → (𝑥𝑦) ∈ 𝑀)
8079expcom 451 . . . . . . . . . 10 ((𝑥𝑀𝑦𝑀) → (𝜑 → (𝑥𝑦) ∈ 𝑀))
8174, 77, 80vtocl2ga 3263 . . . . . . . . 9 (((𝐵𝑎) ∈ 𝑀 ∧ (𝐵𝑏) ∈ 𝑀) → (𝜑 → ((𝐵𝑎) ∪ (𝐵𝑏)) ∈ 𝑀))
8281imp 445 . . . . . . . 8 ((((𝐵𝑎) ∈ 𝑀 ∧ (𝐵𝑏) ∈ 𝑀) ∧ 𝜑) → ((𝐵𝑎) ∪ (𝐵𝑏)) ∈ 𝑀)
8369, 70, 71, 82syl21anc 1322 . . . . . . 7 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → ((𝐵𝑎) ∪ (𝐵𝑏)) ∈ 𝑀)
8467, 83syl5eqel 2702 . . . . . 6 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝐵 ∖ (𝑎𝑏)) ∈ 𝑀)
85 difeq2 3705 . . . . . . . 8 (𝑧 = (𝑎𝑏) → (𝐵𝑧) = (𝐵 ∖ (𝑎𝑏)))
8685eleq1d 2683 . . . . . . 7 (𝑧 = (𝑎𝑏) → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝑎𝑏)) ∈ 𝑀))
8786, 5elrab2 3352 . . . . . 6 ((𝑎𝑏) ∈ 𝐽 ↔ ((𝑎𝑏) ∈ 𝒫 𝐵 ∧ (𝐵 ∖ (𝑎𝑏)) ∈ 𝑀))
8866, 84, 87sylanbrc 697 . . . . 5 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝑎𝑏) ∈ 𝐽)
8988ralrimivva 2966 . . . 4 (𝜑 → ∀𝑎𝐽𝑏𝐽 (𝑎𝑏) ∈ 𝐽)
90 pwexg 4815 . . . . . . 7 (𝐵𝑀 → 𝒫 𝐵 ∈ V)
9144, 90syl 17 . . . . . 6 (𝜑 → 𝒫 𝐵 ∈ V)
925, 91rabexd 4779 . . . . 5 (𝜑𝐽 ∈ V)
93 istopg 20632 . . . . 5 (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑎(𝑎𝐽 𝑎𝐽) ∧ ∀𝑎𝐽𝑏𝐽 (𝑎𝑏) ∈ 𝐽)))
9492, 93syl 17 . . . 4 (𝜑 → (𝐽 ∈ Top ↔ (∀𝑎(𝑎𝐽 𝑎𝐽) ∧ ∀𝑎𝐽𝑏𝐽 (𝑎𝑏) ∈ 𝐽)))
9554, 89, 94mpbir2and 956 . . 3 (𝜑𝐽 ∈ Top)
967unissi 4432 . . . . . 6 𝐽 𝒫 𝐵
97 unipw 4884 . . . . . 6 𝒫 𝐵 = 𝐵
9896, 97sseqtri 3621 . . . . 5 𝐽𝐵
99 pwidg 4149 . . . . . . 7 (𝐵𝑀𝐵 ∈ 𝒫 𝐵)
10044, 99syl 17 . . . . . 6 (𝜑𝐵 ∈ 𝒫 𝐵)
101 difid 3927 . . . . . . 7 (𝐵𝐵) = ∅
102 mretopd.z . . . . . . 7 (𝜑 → ∅ ∈ 𝑀)
103101, 102syl5eqel 2702 . . . . . 6 (𝜑 → (𝐵𝐵) ∈ 𝑀)
104 difeq2 3705 . . . . . . . 8 (𝑧 = 𝐵 → (𝐵𝑧) = (𝐵𝐵))
105104eleq1d 2683 . . . . . . 7 (𝑧 = 𝐵 → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵𝐵) ∈ 𝑀))
106105, 5elrab2 3352 . . . . . 6 (𝐵𝐽 ↔ (𝐵 ∈ 𝒫 𝐵 ∧ (𝐵𝐵) ∈ 𝑀))
107100, 103, 106sylanbrc 697 . . . . 5 (𝜑𝐵𝐽)
108 unissel 4439 . . . . 5 (( 𝐽𝐵𝐵𝐽) → 𝐽 = 𝐵)
10998, 107, 108sylancr 694 . . . 4 (𝜑 𝐽 = 𝐵)
110109eqcomd 2627 . . 3 (𝜑𝐵 = 𝐽)
111 istopon 20649 . . 3 (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = 𝐽))
11295, 110, 111sylanbrc 697 . 2 (𝜑𝐽 ∈ (TopOn‘𝐵))
113 eqid 2621 . . . . 5 𝐽 = 𝐽
114113cldval 20750 . . . 4 (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 𝐽 ∣ ( 𝐽𝑥) ∈ 𝐽})
11595, 114syl 17 . . 3 (𝜑 → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 𝐽 ∣ ( 𝐽𝑥) ∈ 𝐽})
116109pweqd 4140 . . . 4 (𝜑 → 𝒫 𝐽 = 𝒫 𝐵)
117109difeq1d 3710 . . . . 5 (𝜑 → ( 𝐽𝑥) = (𝐵𝑥))
118117eleq1d 2683 . . . 4 (𝜑 → (( 𝐽𝑥) ∈ 𝐽 ↔ (𝐵𝑥) ∈ 𝐽))
119116, 118rabeqbidv 3184 . . 3 (𝜑 → {𝑥 ∈ 𝒫 𝐽 ∣ ( 𝐽𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵𝑥) ∈ 𝐽})
1205eleq2i 2690 . . . . . . 7 ((𝐵𝑥) ∈ 𝐽 ↔ (𝐵𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀})
121 difss 3720 . . . . . . . . . 10 (𝐵𝑥) ⊆ 𝐵
122 elpw2g 4792 . . . . . . . . . . 11 (𝐵𝑀 → ((𝐵𝑥) ∈ 𝒫 𝐵 ↔ (𝐵𝑥) ⊆ 𝐵))
12344, 122syl 17 . . . . . . . . . 10 (𝜑 → ((𝐵𝑥) ∈ 𝒫 𝐵 ↔ (𝐵𝑥) ⊆ 𝐵))
124121, 123mpbiri 248 . . . . . . . . 9 (𝜑 → (𝐵𝑥) ∈ 𝒫 𝐵)
125 difeq2 3705 . . . . . . . . . . 11 (𝑧 = (𝐵𝑥) → (𝐵𝑧) = (𝐵 ∖ (𝐵𝑥)))
126125eleq1d 2683 . . . . . . . . . 10 (𝑧 = (𝐵𝑥) → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝐵𝑥)) ∈ 𝑀))
127126elrab3 3351 . . . . . . . . 9 ((𝐵𝑥) ∈ 𝒫 𝐵 → ((𝐵𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵𝑥)) ∈ 𝑀))
128124, 127syl 17 . . . . . . . 8 (𝜑 → ((𝐵𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵𝑥)) ∈ 𝑀))
129128adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ 𝒫 𝐵) → ((𝐵𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵𝑥)) ∈ 𝑀))
130120, 129syl5bb 272 . . . . . 6 ((𝜑𝑥 ∈ 𝒫 𝐵) → ((𝐵𝑥) ∈ 𝐽 ↔ (𝐵 ∖ (𝐵𝑥)) ∈ 𝑀))
131 elpwi 4145 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
132 dfss4 3841 . . . . . . . . 9 (𝑥𝐵 ↔ (𝐵 ∖ (𝐵𝑥)) = 𝑥)
133131, 132sylib 208 . . . . . . . 8 (𝑥 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵𝑥)) = 𝑥)
134133adantl 482 . . . . . . 7 ((𝜑𝑥 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵𝑥)) = 𝑥)
135134eleq1d 2683 . . . . . 6 ((𝜑𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐵𝑥)) ∈ 𝑀𝑥𝑀))
136130, 135bitrd 268 . . . . 5 ((𝜑𝑥 ∈ 𝒫 𝐵) → ((𝐵𝑥) ∈ 𝐽𝑥𝑀))
137136rabbidva 3179 . . . 4 (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵𝑥𝑀})
138 incom 3788 . . . . . 6 (𝑀 ∩ 𝒫 𝐵) = (𝒫 𝐵𝑀)
139 dfin5 3567 . . . . . 6 (𝒫 𝐵𝑀) = {𝑥 ∈ 𝒫 𝐵𝑥𝑀}
140138, 139eqtri 2643 . . . . 5 (𝑀 ∩ 𝒫 𝐵) = {𝑥 ∈ 𝒫 𝐵𝑥𝑀}
141 mresspw 16184 . . . . . . 7 (𝑀 ∈ (Moore‘𝐵) → 𝑀 ⊆ 𝒫 𝐵)
14221, 141syl 17 . . . . . 6 (𝜑𝑀 ⊆ 𝒫 𝐵)
143 df-ss 3573 . . . . . 6 (𝑀 ⊆ 𝒫 𝐵 ↔ (𝑀 ∩ 𝒫 𝐵) = 𝑀)
144142, 143sylib 208 . . . . 5 (𝜑 → (𝑀 ∩ 𝒫 𝐵) = 𝑀)
145140, 144syl5eqr 2669 . . . 4 (𝜑 → {𝑥 ∈ 𝒫 𝐵𝑥𝑀} = 𝑀)
146137, 145eqtrd 2655 . . 3 (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵𝑥) ∈ 𝐽} = 𝑀)
147115, 119, 1463eqtrrd 2660 . 2 (𝜑𝑀 = (Clsd‘𝐽))
148112, 147jca 554 1 (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036  ∀wal 1478   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  {crab 2911  Vcvv 3189   ∖ cdif 3556   ∪ cun 3557   ∩ cin 3558   ⊆ wss 3559  ∅c0 3896  𝒫 cpw 4135  ∪ cuni 4407  ∪ ciun 4490  ∩ ciin 4491  ‘cfv 5852  Moorecmre 16174  Topctop 20630  TopOnctopon 20647  Clsdccld 20743 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-iota 5815  df-fun 5854  df-fv 5860  df-mre 16178  df-top 20631  df-topon 20648  df-cld 20746 This theorem is referenced by:  iscldtop  20822  istopclsd  36778
 Copyright terms: Public domain W3C validator