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 ) ) )