This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mretopd

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)

Ref Expression
Hypotheses mretopd.m ⊢ ( 𝜑 → 𝑀 ∈ ( Moore ‘ 𝐵 ) )
mretopd.z ⊢ ( 𝜑 → ∅ ∈ 𝑀 )
mretopd.u ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 )
mretopd.j ⊢ 𝐽 = { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 }
Assertion mretopd ( 𝜑 → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝑀 = ( Clsd ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 mretopd.m ⊢ ( 𝜑 → 𝑀 ∈ ( Moore ‘ 𝐵 ) )
2 mretopd.z ⊢ ( 𝜑 → ∅ ∈ 𝑀 )
3 mretopd.u ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 )
4 mretopd.j ⊢ 𝐽 = { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 }
5 unieq ⊢ ( 𝑎 = ∅ → ∪ 𝑎 = ∪ ∅ )
6 uni0 ⊢ ∪ ∅ = ∅
7 5 6 eqtrdi ⊢ ( 𝑎 = ∅ → ∪ 𝑎 = ∅ )
8 7 eleq1d ⊢ ( 𝑎 = ∅ → ( ∪ 𝑎 ∈ 𝐽 ↔ ∅ ∈ 𝐽 ) )
9 4 ssrab3 ⊢ 𝐽 ⊆ 𝒫 𝐵
10 sstr ⊢ ( ( 𝑎 ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝐵 ) → 𝑎 ⊆ 𝒫 𝐵 )
11 9 10 mpan2 ⊢ ( 𝑎 ⊆ 𝐽 → 𝑎 ⊆ 𝒫 𝐵 )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → 𝑎 ⊆ 𝒫 𝐵 )
13 sspwuni ⊢ ( 𝑎 ⊆ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵 )
14 12 13 sylib ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ∪ 𝑎 ⊆ 𝐵 )
15 vuniex ⊢ ∪ 𝑎 ∈ V
16 15 elpw ⊢ ( ∪ 𝑎 ∈ 𝒫 𝐵 ↔ ∪ 𝑎 ⊆ 𝐵 )
17 14 16 sylibr ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ∪ 𝑎 ∈ 𝒫 𝐵 )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ∪ 𝑎 ∈ 𝒫 𝐵 )
19 uniiun ⊢ ∪ 𝑎 = ∪ 𝑏 ∈ 𝑎 𝑏
20 19 difeq2i ⊢ ( 𝐵 ∖ ∪ 𝑎 ) = ( 𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏 )
21 iindif2 ⊢ ( 𝑎 ≠ ∅ → ∩ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) = ( 𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏 ) )
22 21 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ∩ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) = ( 𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏 ) )
23 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → 𝑀 ∈ ( Moore ‘ 𝐵 ) )
24 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → 𝑎 ≠ ∅ )
25 difeq2 ⊢ ( 𝑧 = 𝑏 → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ 𝑏 ) )
26 25 eleq1d ⊢ ( 𝑧 = 𝑏 → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) )
27 26 4 elrab2 ⊢ ( 𝑏 ∈ 𝐽 ↔ ( 𝑏 ∈ 𝒫 𝐵 ∧ ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) )
28 27 simprbi ⊢ ( 𝑏 ∈ 𝐽 → ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
29 28 rgen ⊢ ∀ 𝑏 ∈ 𝐽 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀
30 ssralv ⊢ ( 𝑎 ⊆ 𝐽 → ( ∀ 𝑏 ∈ 𝐽 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 → ∀ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ( ∀ 𝑏 ∈ 𝐽 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 → ∀ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) )
32 29 31 mpi ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ∀ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ∀ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
34 mreiincl ⊢ ( ( 𝑀 ∈ ( Moore ‘ 𝐵 ) ∧ 𝑎 ≠ ∅ ∧ ∀ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) → ∩ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
35 23 24 33 34 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ∩ 𝑏 ∈ 𝑎 ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
36 22 35 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ( 𝐵 ∖ ∪ 𝑏 ∈ 𝑎 𝑏 ) ∈ 𝑀 )
37 20 36 eqeltrid ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ( 𝐵 ∖ ∪ 𝑎 ) ∈ 𝑀 )
38 difeq2 ⊢ ( 𝑧 = ∪ 𝑎 → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ ∪ 𝑎 ) )
39 38 eleq1d ⊢ ( 𝑧 = ∪ 𝑎 → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ ∪ 𝑎 ) ∈ 𝑀 ) )
40 39 4 elrab2 ⊢ ( ∪ 𝑎 ∈ 𝐽 ↔ ( ∪ 𝑎 ∈ 𝒫 𝐵 ∧ ( 𝐵 ∖ ∪ 𝑎 ) ∈ 𝑀 ) )
41 18 37 40 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑎 ≠ ∅ ) → ∪ 𝑎 ∈ 𝐽 )
42 0elpw ⊢ ∅ ∈ 𝒫 𝐵
43 42 a1i ⊢ ( 𝜑 → ∅ ∈ 𝒫 𝐵 )
44 mre1cl ⊢ ( 𝑀 ∈ ( Moore ‘ 𝐵 ) → 𝐵 ∈ 𝑀 )
45 1 44 syl ⊢ ( 𝜑 → 𝐵 ∈ 𝑀 )
46 difeq2 ⊢ ( 𝑧 = ∅ → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ ∅ ) )
47 dif0 ⊢ ( 𝐵 ∖ ∅ ) = 𝐵
48 46 47 eqtrdi ⊢ ( 𝑧 = ∅ → ( 𝐵 ∖ 𝑧 ) = 𝐵 )
49 48 eleq1d ⊢ ( 𝑧 = ∅ → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ 𝐵 ∈ 𝑀 ) )
50 49 4 elrab2 ⊢ ( ∅ ∈ 𝐽 ↔ ( ∅ ∈ 𝒫 𝐵 ∧ 𝐵 ∈ 𝑀 ) )
51 43 45 50 sylanbrc ⊢ ( 𝜑 → ∅ ∈ 𝐽 )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ∅ ∈ 𝐽 )
53 8 41 52 pm2.61ne ⊢ ( ( 𝜑 ∧ 𝑎 ⊆ 𝐽 ) → ∪ 𝑎 ∈ 𝐽 )
54 53 ex ⊢ ( 𝜑 → ( 𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽 ) )
55 54 alrimiv ⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽 ) )
56 inss1 ⊢ ( 𝑎 ∩ 𝑏 ) ⊆ 𝑎
57 difeq2 ⊢ ( 𝑧 = 𝑎 → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ 𝑎 ) )
58 57 eleq1d ⊢ ( 𝑧 = 𝑎 → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 ) )
59 58 4 elrab2 ⊢ ( 𝑎 ∈ 𝐽 ↔ ( 𝑎 ∈ 𝒫 𝐵 ∧ ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 ) )
60 59 simplbi ⊢ ( 𝑎 ∈ 𝐽 → 𝑎 ∈ 𝒫 𝐵 )
61 60 elpwid ⊢ ( 𝑎 ∈ 𝐽 → 𝑎 ⊆ 𝐵 )
62 61 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → 𝑎 ⊆ 𝐵 )
63 56 62 sstrid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝑎 ∩ 𝑏 ) ⊆ 𝐵 )
64 vex ⊢ 𝑎 ∈ V
65 64 inex1 ⊢ ( 𝑎 ∩ 𝑏 ) ∈ V
66 65 elpw ⊢ ( ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐵 ↔ ( 𝑎 ∩ 𝑏 ) ⊆ 𝐵 )
67 63 66 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐵 )
68 difindi ⊢ ( 𝐵 ∖ ( 𝑎 ∩ 𝑏 ) ) = ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) )
69 59 simprbi ⊢ ( 𝑎 ∈ 𝐽 → ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 )
70 69 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 )
71 28 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 )
72 simpl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → 𝜑 )
73 uneq1 ⊢ ( 𝑥 = ( 𝐵 ∖ 𝑎 ) → ( 𝑥 ∪ 𝑦 ) = ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) )
74 73 eleq1d ⊢ ( 𝑥 = ( 𝐵 ∖ 𝑎 ) → ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 ↔ ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) ∈ 𝑀 ) )
75 74 imbi2d ⊢ ( 𝑥 = ( 𝐵 ∖ 𝑎 ) → ( ( 𝜑 → ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 ) ↔ ( 𝜑 → ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) ∈ 𝑀 ) ) )
76 uneq2 ⊢ ( 𝑦 = ( 𝐵 ∖ 𝑏 ) → ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) = ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) )
77 76 eleq1d ⊢ ( 𝑦 = ( 𝐵 ∖ 𝑏 ) → ( ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) ∈ 𝑀 ↔ ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) ∈ 𝑀 ) )
78 77 imbi2d ⊢ ( 𝑦 = ( 𝐵 ∖ 𝑏 ) → ( ( 𝜑 → ( ( 𝐵 ∖ 𝑎 ) ∪ 𝑦 ) ∈ 𝑀 ) ↔ ( 𝜑 → ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) ∈ 𝑀 ) ) )
79 3 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 )
80 79 expcom ⊢ ( ( 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀 ) → ( 𝜑 → ( 𝑥 ∪ 𝑦 ) ∈ 𝑀 ) )
81 75 78 80 vtocl2ga ⊢ ( ( ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 ∧ ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) → ( 𝜑 → ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) ∈ 𝑀 ) )
82 81 imp ⊢ ( ( ( ( 𝐵 ∖ 𝑎 ) ∈ 𝑀 ∧ ( 𝐵 ∖ 𝑏 ) ∈ 𝑀 ) ∧ 𝜑 ) → ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) ∈ 𝑀 )
83 70 71 72 82 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( ( 𝐵 ∖ 𝑎 ) ∪ ( 𝐵 ∖ 𝑏 ) ) ∈ 𝑀 )
84 68 83 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝐵 ∖ ( 𝑎 ∩ 𝑏 ) ) ∈ 𝑀 )
85 difeq2 ⊢ ( 𝑧 = ( 𝑎 ∩ 𝑏 ) → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ ( 𝑎 ∩ 𝑏 ) ) )
86 85 eleq1d ⊢ ( 𝑧 = ( 𝑎 ∩ 𝑏 ) → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ ( 𝑎 ∩ 𝑏 ) ) ∈ 𝑀 ) )
87 86 4 elrab2 ⊢ ( ( 𝑎 ∩ 𝑏 ) ∈ 𝐽 ↔ ( ( 𝑎 ∩ 𝑏 ) ∈ 𝒫 𝐵 ∧ ( 𝐵 ∖ ( 𝑎 ∩ 𝑏 ) ) ∈ 𝑀 ) )
88 67 84 87 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐽 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝐽 )
89 88 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐽 ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∩ 𝑏 ) ∈ 𝐽 )
90 45 pwexd ⊢ ( 𝜑 → 𝒫 𝐵 ∈ V )
91 4 90 rabexd ⊢ ( 𝜑 → 𝐽 ∈ V )
92 istopg ⊢ ( 𝐽 ∈ V → ( 𝐽 ∈ Top ↔ ( ∀ 𝑎 ( 𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽 ) ∧ ∀ 𝑎 ∈ 𝐽 ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∩ 𝑏 ) ∈ 𝐽 ) ) )
93 91 92 syl ⊢ ( 𝜑 → ( 𝐽 ∈ Top ↔ ( ∀ 𝑎 ( 𝑎 ⊆ 𝐽 → ∪ 𝑎 ∈ 𝐽 ) ∧ ∀ 𝑎 ∈ 𝐽 ∀ 𝑏 ∈ 𝐽 ( 𝑎 ∩ 𝑏 ) ∈ 𝐽 ) ) )
94 55 89 93 mpbir2and ⊢ ( 𝜑 → 𝐽 ∈ Top )
95 9 unissi ⊢ ∪ 𝐽 ⊆ ∪ 𝒫 𝐵
96 unipw ⊢ ∪ 𝒫 𝐵 = 𝐵
97 95 96 sseqtri ⊢ ∪ 𝐽 ⊆ 𝐵
98 pwidg ⊢ ( 𝐵 ∈ 𝑀 → 𝐵 ∈ 𝒫 𝐵 )
99 45 98 syl ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐵 )
100 difid ⊢ ( 𝐵 ∖ 𝐵 ) = ∅
101 100 2 eqeltrid ⊢ ( 𝜑 → ( 𝐵 ∖ 𝐵 ) ∈ 𝑀 )
102 difeq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ 𝐵 ) )
103 102 eleq1d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ 𝐵 ) ∈ 𝑀 ) )
104 103 4 elrab2 ⊢ ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ∈ 𝒫 𝐵 ∧ ( 𝐵 ∖ 𝐵 ) ∈ 𝑀 ) )
105 99 101 104 sylanbrc ⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
106 unissel ⊢ ( ( ∪ 𝐽 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐽 ) → ∪ 𝐽 = 𝐵 )
107 97 105 106 sylancr ⊢ ( 𝜑 → ∪ 𝐽 = 𝐵 )
108 107 eqcomd ⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
109 istopon ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽 ) )
110 94 108 109 sylanbrc ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
111 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
112 111 cldval ⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) = { 𝑥 ∈ 𝒫 ∪ 𝐽 ∣ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 } )
113 94 112 syl ⊢ ( 𝜑 → ( Clsd ‘ 𝐽 ) = { 𝑥 ∈ 𝒫 ∪ 𝐽 ∣ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 } )
114 107 pweqd ⊢ ( 𝜑 → 𝒫 ∪ 𝐽 = 𝒫 𝐵 )
115 107 difeq1d ⊢ ( 𝜑 → ( ∪ 𝐽 ∖ 𝑥 ) = ( 𝐵 ∖ 𝑥 ) )
116 115 eleq1d ⊢ ( 𝜑 → ( ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ↔ ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 ) )
117 114 116 rabeqbidv ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 ∪ 𝐽 ∣ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 } = { 𝑥 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 } )
118 4 eleq2i ⊢ ( ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 ↔ ( 𝐵 ∖ 𝑥 ) ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 } )
119 difss ⊢ ( 𝐵 ∖ 𝑥 ) ⊆ 𝐵
120 elpw2g ⊢ ( 𝐵 ∈ 𝑀 → ( ( 𝐵 ∖ 𝑥 ) ∈ 𝒫 𝐵 ↔ ( 𝐵 ∖ 𝑥 ) ⊆ 𝐵 ) )
121 45 120 syl ⊢ ( 𝜑 → ( ( 𝐵 ∖ 𝑥 ) ∈ 𝒫 𝐵 ↔ ( 𝐵 ∖ 𝑥 ) ⊆ 𝐵 ) )
122 119 121 mpbiri ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑥 ) ∈ 𝒫 𝐵 )
123 difeq2 ⊢ ( 𝑧 = ( 𝐵 ∖ 𝑥 ) → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) )
124 123 eleq1d ⊢ ( 𝑧 = ( 𝐵 ∖ 𝑥 ) → ( ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ) )
125 124 elrab3 ⊢ ( ( 𝐵 ∖ 𝑥 ) ∈ 𝒫 𝐵 → ( ( 𝐵 ∖ 𝑥 ) ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 } ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ) )
126 122 125 syl ⊢ ( 𝜑 → ( ( 𝐵 ∖ 𝑥 ) ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 } ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ) )
127 126 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ 𝑥 ) ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑧 ) ∈ 𝑀 } ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ) )
128 118 127 bitrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ) )
129 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵 )
130 dfss4 ⊢ ( 𝑥 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) = 𝑥 )
131 129 130 sylib ⊢ ( 𝑥 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) = 𝑥 )
132 131 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) = 𝑥 )
133 132 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ ( 𝐵 ∖ 𝑥 ) ) ∈ 𝑀 ↔ 𝑥 ∈ 𝑀 ) )
134 128 133 bitrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 ↔ 𝑥 ∈ 𝑀 ) )
135 134 rabbidva ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 } = { 𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀 } )
136 incom ⊢ ( 𝑀 ∩ 𝒫 𝐵 ) = ( 𝒫 𝐵 ∩ 𝑀 )
137 dfin5 ⊢ ( 𝒫 𝐵 ∩ 𝑀 ) = { 𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀 }
138 136 137 eqtri ⊢ ( 𝑀 ∩ 𝒫 𝐵 ) = { 𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀 }
139 mresspw ⊢ ( 𝑀 ∈ ( Moore ‘ 𝐵 ) → 𝑀 ⊆ 𝒫 𝐵 )
140 1 139 syl ⊢ ( 𝜑 → 𝑀 ⊆ 𝒫 𝐵 )
141 dfss2 ⊢ ( 𝑀 ⊆ 𝒫 𝐵 ↔ ( 𝑀 ∩ 𝒫 𝐵 ) = 𝑀 )
142 140 141 sylib ⊢ ( 𝜑 → ( 𝑀 ∩ 𝒫 𝐵 ) = 𝑀 )
143 138 142 eqtr3id ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐵 ∣ 𝑥 ∈ 𝑀 } = 𝑀 )
144 135 143 eqtrd ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝐵 ∣ ( 𝐵 ∖ 𝑥 ) ∈ 𝐽 } = 𝑀 )
145 113 117 144 3eqtrrd ⊢ ( 𝜑 → 𝑀 = ( Clsd ‘ 𝐽 ) )
146 110 145 jca ⊢ ( 𝜑 → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝑀 = ( Clsd ‘ 𝐽 ) ) )