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 
|- ( ph -> M e. ( Moore ` B ) )
mretopd.z 
|- ( ph -> (/) e. M )
mretopd.u 
|- ( ( ph /\ x e. M /\ y e. M ) -> ( x u. y ) e. M )
mretopd.j 
|- J = { z e. ~P B | ( B \ z ) e. M }
Assertion mretopd 
|- ( ph -> ( J e. ( TopOn ` B ) /\ M = ( Clsd ` J ) ) )

Proof

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