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 syl5bb ( ( 𝜑𝑥 ∈ 𝒫 𝐵 ) → ( ( 𝐵𝑥 ) ∈ 𝐽 ↔ ( 𝐵 ∖ ( 𝐵𝑥 ) ) ∈ 𝑀 ) )
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 df-ss ( 𝑀 ⊆ 𝒫 𝐵 ↔ ( 𝑀 ∩ 𝒫 𝐵 ) = 𝑀 )
142 140 141 sylib ( 𝜑 → ( 𝑀 ∩ 𝒫 𝐵 ) = 𝑀 )
143 138 142 eqtr3id ( 𝜑 → { 𝑥 ∈ 𝒫 𝐵𝑥𝑀 } = 𝑀 )
144 135 143 eqtrd ( 𝜑 → { 𝑥 ∈ 𝒫 𝐵 ∣ ( 𝐵𝑥 ) ∈ 𝐽 } = 𝑀 )
145 113 117 144 3eqtrrd ( 𝜑𝑀 = ( Clsd ‘ 𝐽 ) )
146 110 145 jca ( 𝜑 → ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝑀 = ( Clsd ‘ 𝐽 ) ) )