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

Theorem mretopd 21836
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 4804 . . . . . . . . 9 (𝑎 = ∅ → 𝑎 = ∅)
2 uni0 4823 . . . . . . . . 9 ∅ = ∅
31, 2eqtrdi 2789 . . . . . . . 8 (𝑎 = ∅ → 𝑎 = ∅)
43eleq1d 2817 . . . . . . 7 (𝑎 = ∅ → ( 𝑎𝐽 ↔ ∅ ∈ 𝐽))
5 mretopd.j . . . . . . . . . . . . . 14 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀}
65ssrab3 3969 . . . . . . . . . . . . 13 𝐽 ⊆ 𝒫 𝐵
7 sstr 3883 . . . . . . . . . . . . 13 ((𝑎𝐽𝐽 ⊆ 𝒫 𝐵) → 𝑎 ⊆ 𝒫 𝐵)
86, 7mpan2 691 . . . . . . . . . . . 12 (𝑎𝐽𝑎 ⊆ 𝒫 𝐵)
98adantl 485 . . . . . . . . . . 11 ((𝜑𝑎𝐽) → 𝑎 ⊆ 𝒫 𝐵)
10 sspwuni 4982 . . . . . . . . . . 11 (𝑎 ⊆ 𝒫 𝐵 𝑎𝐵)
119, 10sylib 221 . . . . . . . . . 10 ((𝜑𝑎𝐽) → 𝑎𝐵)
12 vuniex 7477 . . . . . . . . . . 11 𝑎 ∈ V
1312elpw 4489 . . . . . . . . . 10 ( 𝑎 ∈ 𝒫 𝐵 𝑎𝐵)
1411, 13sylibr 237 . . . . . . . . 9 ((𝜑𝑎𝐽) → 𝑎 ∈ 𝒫 𝐵)
1514adantr 484 . . . . . . . 8 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑎 ∈ 𝒫 𝐵)
16 uniiun 4941 . . . . . . . . . 10 𝑎 = 𝑏𝑎 𝑏
1716difeq2i 4008 . . . . . . . . 9 (𝐵 𝑎) = (𝐵 𝑏𝑎 𝑏)
18 iindif2 4959 . . . . . . . . . . 11 (𝑎 ≠ ∅ → 𝑏𝑎 (𝐵𝑏) = (𝐵 𝑏𝑎 𝑏))
1918adantl 485 . . . . . . . . . 10 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑏𝑎 (𝐵𝑏) = (𝐵 𝑏𝑎 𝑏))
20 mretopd.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ (Moore‘𝐵))
2120ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑀 ∈ (Moore‘𝐵))
22 simpr 488 . . . . . . . . . . 11 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑎 ≠ ∅)
23 difeq2 4005 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑏 → (𝐵𝑧) = (𝐵𝑏))
2423eleq1d 2817 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑏 → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵𝑏) ∈ 𝑀))
2524, 5elrab2 3588 . . . . . . . . . . . . . . 15 (𝑏𝐽 ↔ (𝑏 ∈ 𝒫 𝐵 ∧ (𝐵𝑏) ∈ 𝑀))
2625simprbi 500 . . . . . . . . . . . . . 14 (𝑏𝐽 → (𝐵𝑏) ∈ 𝑀)
2726rgen 3063 . . . . . . . . . . . . 13 𝑏𝐽 (𝐵𝑏) ∈ 𝑀
28 ssralv 3941 . . . . . . . . . . . . . 14 (𝑎𝐽 → (∀𝑏𝐽 (𝐵𝑏) ∈ 𝑀 → ∀𝑏𝑎 (𝐵𝑏) ∈ 𝑀))
2928adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑎𝐽) → (∀𝑏𝐽 (𝐵𝑏) ∈ 𝑀 → ∀𝑏𝑎 (𝐵𝑏) ∈ 𝑀))
3027, 29mpi 20 . . . . . . . . . . . 12 ((𝜑𝑎𝐽) → ∀𝑏𝑎 (𝐵𝑏) ∈ 𝑀)
3130adantr 484 . . . . . . . . . . 11 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → ∀𝑏𝑎 (𝐵𝑏) ∈ 𝑀)
32 mreiincl 16963 . . . . . . . . . . 11 ((𝑀 ∈ (Moore‘𝐵) ∧ 𝑎 ≠ ∅ ∧ ∀𝑏𝑎 (𝐵𝑏) ∈ 𝑀) → 𝑏𝑎 (𝐵𝑏) ∈ 𝑀)
3321, 22, 31, 32syl3anc 1372 . . . . . . . . . 10 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑏𝑎 (𝐵𝑏) ∈ 𝑀)
3419, 33eqeltrrd 2834 . . . . . . . . 9 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 𝑏𝑎 𝑏) ∈ 𝑀)
3517, 34eqeltrid 2837 . . . . . . . 8 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → (𝐵 𝑎) ∈ 𝑀)
36 difeq2 4005 . . . . . . . . . 10 (𝑧 = 𝑎 → (𝐵𝑧) = (𝐵 𝑎))
3736eleq1d 2817 . . . . . . . . 9 (𝑧 = 𝑎 → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵 𝑎) ∈ 𝑀))
3837, 5elrab2 3588 . . . . . . . 8 ( 𝑎𝐽 ↔ ( 𝑎 ∈ 𝒫 𝐵 ∧ (𝐵 𝑎) ∈ 𝑀))
3915, 35, 38sylanbrc 586 . . . . . . 7 (((𝜑𝑎𝐽) ∧ 𝑎 ≠ ∅) → 𝑎𝐽)
40 0elpw 5219 . . . . . . . . . 10 ∅ ∈ 𝒫 𝐵
4140a1i 11 . . . . . . . . 9 (𝜑 → ∅ ∈ 𝒫 𝐵)
42 mre1cl 16961 . . . . . . . . . 10 (𝑀 ∈ (Moore‘𝐵) → 𝐵𝑀)
4320, 42syl 17 . . . . . . . . 9 (𝜑𝐵𝑀)
44 difeq2 4005 . . . . . . . . . . . 12 (𝑧 = ∅ → (𝐵𝑧) = (𝐵 ∖ ∅))
45 dif0 4259 . . . . . . . . . . . 12 (𝐵 ∖ ∅) = 𝐵
4644, 45eqtrdi 2789 . . . . . . . . . . 11 (𝑧 = ∅ → (𝐵𝑧) = 𝐵)
4746eleq1d 2817 . . . . . . . . . 10 (𝑧 = ∅ → ((𝐵𝑧) ∈ 𝑀𝐵𝑀))
4847, 5elrab2 3588 . . . . . . . . 9 (∅ ∈ 𝐽 ↔ (∅ ∈ 𝒫 𝐵𝐵𝑀))
4941, 43, 48sylanbrc 586 . . . . . . . 8 (𝜑 → ∅ ∈ 𝐽)
5049adantr 484 . . . . . . 7 ((𝜑𝑎𝐽) → ∅ ∈ 𝐽)
514, 39, 50pm2.61ne 3019 . . . . . 6 ((𝜑𝑎𝐽) → 𝑎𝐽)
5251ex 416 . . . . 5 (𝜑 → (𝑎𝐽 𝑎𝐽))
5352alrimiv 1933 . . . 4 (𝜑 → ∀𝑎(𝑎𝐽 𝑎𝐽))
54 inss1 4117 . . . . . . . 8 (𝑎𝑏) ⊆ 𝑎
55 difeq2 4005 . . . . . . . . . . . . 13 (𝑧 = 𝑎 → (𝐵𝑧) = (𝐵𝑎))
5655eleq1d 2817 . . . . . . . . . . . 12 (𝑧 = 𝑎 → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵𝑎) ∈ 𝑀))
5756, 5elrab2 3588 . . . . . . . . . . 11 (𝑎𝐽 ↔ (𝑎 ∈ 𝒫 𝐵 ∧ (𝐵𝑎) ∈ 𝑀))
5857simplbi 501 . . . . . . . . . 10 (𝑎𝐽𝑎 ∈ 𝒫 𝐵)
5958elpwid 4496 . . . . . . . . 9 (𝑎𝐽𝑎𝐵)
6059ad2antrl 728 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → 𝑎𝐵)
6154, 60sstrid 3886 . . . . . . 7 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝑎𝑏) ⊆ 𝐵)
62 vex 3401 . . . . . . . . 9 𝑎 ∈ V
6362inex1 5182 . . . . . . . 8 (𝑎𝑏) ∈ V
6463elpw 4489 . . . . . . 7 ((𝑎𝑏) ∈ 𝒫 𝐵 ↔ (𝑎𝑏) ⊆ 𝐵)
6561, 64sylibr 237 . . . . . 6 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝑎𝑏) ∈ 𝒫 𝐵)
66 difindi 4170 . . . . . . 7 (𝐵 ∖ (𝑎𝑏)) = ((𝐵𝑎) ∪ (𝐵𝑏))
6757simprbi 500 . . . . . . . . 9 (𝑎𝐽 → (𝐵𝑎) ∈ 𝑀)
6867ad2antrl 728 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝐵𝑎) ∈ 𝑀)
6926ad2antll 729 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝐵𝑏) ∈ 𝑀)
70 simpl 486 . . . . . . . 8 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → 𝜑)
71 uneq1 4044 . . . . . . . . . . . 12 (𝑥 = (𝐵𝑎) → (𝑥𝑦) = ((𝐵𝑎) ∪ 𝑦))
7271eleq1d 2817 . . . . . . . . . . 11 (𝑥 = (𝐵𝑎) → ((𝑥𝑦) ∈ 𝑀 ↔ ((𝐵𝑎) ∪ 𝑦) ∈ 𝑀))
7372imbi2d 344 . . . . . . . . . 10 (𝑥 = (𝐵𝑎) → ((𝜑 → (𝑥𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵𝑎) ∪ 𝑦) ∈ 𝑀)))
74 uneq2 4045 . . . . . . . . . . . 12 (𝑦 = (𝐵𝑏) → ((𝐵𝑎) ∪ 𝑦) = ((𝐵𝑎) ∪ (𝐵𝑏)))
7574eleq1d 2817 . . . . . . . . . . 11 (𝑦 = (𝐵𝑏) → (((𝐵𝑎) ∪ 𝑦) ∈ 𝑀 ↔ ((𝐵𝑎) ∪ (𝐵𝑏)) ∈ 𝑀))
7675imbi2d 344 . . . . . . . . . 10 (𝑦 = (𝐵𝑏) → ((𝜑 → ((𝐵𝑎) ∪ 𝑦) ∈ 𝑀) ↔ (𝜑 → ((𝐵𝑎) ∪ (𝐵𝑏)) ∈ 𝑀)))
77 mretopd.u . . . . . . . . . . . 12 ((𝜑𝑥𝑀𝑦𝑀) → (𝑥𝑦) ∈ 𝑀)
78773expb 1121 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑀𝑦𝑀)) → (𝑥𝑦) ∈ 𝑀)
7978expcom 417 . . . . . . . . . 10 ((𝑥𝑀𝑦𝑀) → (𝜑 → (𝑥𝑦) ∈ 𝑀))
8073, 76, 79vtocl2ga 3478 . . . . . . . . 9 (((𝐵𝑎) ∈ 𝑀 ∧ (𝐵𝑏) ∈ 𝑀) → (𝜑 → ((𝐵𝑎) ∪ (𝐵𝑏)) ∈ 𝑀))
8180imp 410 . . . . . . . 8 ((((𝐵𝑎) ∈ 𝑀 ∧ (𝐵𝑏) ∈ 𝑀) ∧ 𝜑) → ((𝐵𝑎) ∪ (𝐵𝑏)) ∈ 𝑀)
8268, 69, 70, 81syl21anc 837 . . . . . . 7 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → ((𝐵𝑎) ∪ (𝐵𝑏)) ∈ 𝑀)
8366, 82eqeltrid 2837 . . . . . 6 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝐵 ∖ (𝑎𝑏)) ∈ 𝑀)
84 difeq2 4005 . . . . . . . 8 (𝑧 = (𝑎𝑏) → (𝐵𝑧) = (𝐵 ∖ (𝑎𝑏)))
8584eleq1d 2817 . . . . . . 7 (𝑧 = (𝑎𝑏) → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝑎𝑏)) ∈ 𝑀))
8685, 5elrab2 3588 . . . . . 6 ((𝑎𝑏) ∈ 𝐽 ↔ ((𝑎𝑏) ∈ 𝒫 𝐵 ∧ (𝐵 ∖ (𝑎𝑏)) ∈ 𝑀))
8765, 83, 86sylanbrc 586 . . . . 5 ((𝜑 ∧ (𝑎𝐽𝑏𝐽)) → (𝑎𝑏) ∈ 𝐽)
8887ralrimivva 3103 . . . 4 (𝜑 → ∀𝑎𝐽𝑏𝐽 (𝑎𝑏) ∈ 𝐽)
8943pwexd 5243 . . . . . 6 (𝜑 → 𝒫 𝐵 ∈ V)
905, 89rabexd 5198 . . . . 5 (𝜑𝐽 ∈ V)
91 istopg 21639 . . . . 5 (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑎(𝑎𝐽 𝑎𝐽) ∧ ∀𝑎𝐽𝑏𝐽 (𝑎𝑏) ∈ 𝐽)))
9290, 91syl 17 . . . 4 (𝜑 → (𝐽 ∈ Top ↔ (∀𝑎(𝑎𝐽 𝑎𝐽) ∧ ∀𝑎𝐽𝑏𝐽 (𝑎𝑏) ∈ 𝐽)))
9353, 88, 92mpbir2and 713 . . 3 (𝜑𝐽 ∈ Top)
946unissi 4802 . . . . . 6 𝐽 𝒫 𝐵
95 unipw 5306 . . . . . 6 𝒫 𝐵 = 𝐵
9694, 95sseqtri 3911 . . . . 5 𝐽𝐵
97 pwidg 4507 . . . . . . 7 (𝐵𝑀𝐵 ∈ 𝒫 𝐵)
9843, 97syl 17 . . . . . 6 (𝜑𝐵 ∈ 𝒫 𝐵)
99 difid 4257 . . . . . . 7 (𝐵𝐵) = ∅
100 mretopd.z . . . . . . 7 (𝜑 → ∅ ∈ 𝑀)
10199, 100eqeltrid 2837 . . . . . 6 (𝜑 → (𝐵𝐵) ∈ 𝑀)
102 difeq2 4005 . . . . . . . 8 (𝑧 = 𝐵 → (𝐵𝑧) = (𝐵𝐵))
103102eleq1d 2817 . . . . . . 7 (𝑧 = 𝐵 → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵𝐵) ∈ 𝑀))
104103, 5elrab2 3588 . . . . . 6 (𝐵𝐽 ↔ (𝐵 ∈ 𝒫 𝐵 ∧ (𝐵𝐵) ∈ 𝑀))
10598, 101, 104sylanbrc 586 . . . . 5 (𝜑𝐵𝐽)
106 unissel 4826 . . . . 5 (( 𝐽𝐵𝐵𝐽) → 𝐽 = 𝐵)
10796, 105, 106sylancr 590 . . . 4 (𝜑 𝐽 = 𝐵)
108107eqcomd 2744 . . 3 (𝜑𝐵 = 𝐽)
109 istopon 21656 . . 3 (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = 𝐽))
11093, 108, 109sylanbrc 586 . 2 (𝜑𝐽 ∈ (TopOn‘𝐵))
111 eqid 2738 . . . . 5 𝐽 = 𝐽
112111cldval 21767 . . . 4 (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 𝐽 ∣ ( 𝐽𝑥) ∈ 𝐽})
11393, 112syl 17 . . 3 (𝜑 → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 𝐽 ∣ ( 𝐽𝑥) ∈ 𝐽})
114107pweqd 4504 . . . 4 (𝜑 → 𝒫 𝐽 = 𝒫 𝐵)
115107difeq1d 4010 . . . . 5 (𝜑 → ( 𝐽𝑥) = (𝐵𝑥))
116115eleq1d 2817 . . . 4 (𝜑 → (( 𝐽𝑥) ∈ 𝐽 ↔ (𝐵𝑥) ∈ 𝐽))
117114, 116rabeqbidv 3386 . . 3 (𝜑 → {𝑥 ∈ 𝒫 𝐽 ∣ ( 𝐽𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵𝑥) ∈ 𝐽})
1185eleq2i 2824 . . . . . . 7 ((𝐵𝑥) ∈ 𝐽 ↔ (𝐵𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀})
119 difss 4020 . . . . . . . . . 10 (𝐵𝑥) ⊆ 𝐵
120 elpw2g 5209 . . . . . . . . . . 11 (𝐵𝑀 → ((𝐵𝑥) ∈ 𝒫 𝐵 ↔ (𝐵𝑥) ⊆ 𝐵))
12143, 120syl 17 . . . . . . . . . 10 (𝜑 → ((𝐵𝑥) ∈ 𝒫 𝐵 ↔ (𝐵𝑥) ⊆ 𝐵))
122119, 121mpbiri 261 . . . . . . . . 9 (𝜑 → (𝐵𝑥) ∈ 𝒫 𝐵)
123 difeq2 4005 . . . . . . . . . . 11 (𝑧 = (𝐵𝑥) → (𝐵𝑧) = (𝐵 ∖ (𝐵𝑥)))
124123eleq1d 2817 . . . . . . . . . 10 (𝑧 = (𝐵𝑥) → ((𝐵𝑧) ∈ 𝑀 ↔ (𝐵 ∖ (𝐵𝑥)) ∈ 𝑀))
125124elrab3 3586 . . . . . . . . 9 ((𝐵𝑥) ∈ 𝒫 𝐵 → ((𝐵𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵𝑥)) ∈ 𝑀))
126122, 125syl 17 . . . . . . . 8 (𝜑 → ((𝐵𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵𝑥)) ∈ 𝑀))
127126adantr 484 . . . . . . 7 ((𝜑𝑥 ∈ 𝒫 𝐵) → ((𝐵𝑥) ∈ {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵𝑧) ∈ 𝑀} ↔ (𝐵 ∖ (𝐵𝑥)) ∈ 𝑀))
128118, 127syl5bb 286 . . . . . 6 ((𝜑𝑥 ∈ 𝒫 𝐵) → ((𝐵𝑥) ∈ 𝐽 ↔ (𝐵 ∖ (𝐵𝑥)) ∈ 𝑀))
129 elpwi 4494 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
130 dfss4 4147 . . . . . . . . 9 (𝑥𝐵 ↔ (𝐵 ∖ (𝐵𝑥)) = 𝑥)
131129, 130sylib 221 . . . . . . . 8 (𝑥 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵𝑥)) = 𝑥)
132131adantl 485 . . . . . . 7 ((𝜑𝑥 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵𝑥)) = 𝑥)
133132eleq1d 2817 . . . . . 6 ((𝜑𝑥 ∈ 𝒫 𝐵) → ((𝐵 ∖ (𝐵𝑥)) ∈ 𝑀𝑥𝑀))
134128, 133bitrd 282 . . . . 5 ((𝜑𝑥 ∈ 𝒫 𝐵) → ((𝐵𝑥) ∈ 𝐽𝑥𝑀))
135134rabbidva 3378 . . . 4 (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵𝑥) ∈ 𝐽} = {𝑥 ∈ 𝒫 𝐵𝑥𝑀})
136 incom 4089 . . . . . 6 (𝑀 ∩ 𝒫 𝐵) = (𝒫 𝐵𝑀)
137 dfin5 3849 . . . . . 6 (𝒫 𝐵𝑀) = {𝑥 ∈ 𝒫 𝐵𝑥𝑀}
138136, 137eqtri 2761 . . . . 5 (𝑀 ∩ 𝒫 𝐵) = {𝑥 ∈ 𝒫 𝐵𝑥𝑀}
139 mresspw 16959 . . . . . . 7 (𝑀 ∈ (Moore‘𝐵) → 𝑀 ⊆ 𝒫 𝐵)
14020, 139syl 17 . . . . . 6 (𝜑𝑀 ⊆ 𝒫 𝐵)
141 df-ss 3858 . . . . . 6 (𝑀 ⊆ 𝒫 𝐵 ↔ (𝑀 ∩ 𝒫 𝐵) = 𝑀)
142140, 141sylib 221 . . . . 5 (𝜑 → (𝑀 ∩ 𝒫 𝐵) = 𝑀)
143138, 142eqtr3id 2787 . . . 4 (𝜑 → {𝑥 ∈ 𝒫 𝐵𝑥𝑀} = 𝑀)
144135, 143eqtrd 2773 . . 3 (𝜑 → {𝑥 ∈ 𝒫 𝐵 ∣ (𝐵𝑥) ∈ 𝐽} = 𝑀)
145113, 117, 1443eqtrrd 2778 . 2 (𝜑𝑀 = (Clsd‘𝐽))
146110, 145jca 515 1 (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1088  wal 1540   = wceq 1542  wcel 2113  wne 2934  wral 3053  {crab 3057  Vcvv 3397  cdif 3838  cun 3839  cin 3840  wss 3841  c0 4209  𝒫 cpw 4485   cuni 4793   ciun 4878   ciin 4879  cfv 6333  Moorecmre 16949  Topctop 21637  TopOnctopon 21654  Clsdccld 21760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-sbc 3680  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-iin 4881  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-iota 6291  df-fun 6335  df-fv 6341  df-mre 16953  df-top 21638  df-topon 21655  df-cld 21763
This theorem is referenced by:  iscldtop  21839  zartopn  31389  istopclsd  40078
  Copyright terms: Public domain W3C validator