Metamath Proof Explorer

Theorem iscldtop

Description: A family is the closed sets of a topology iff it is a Moore collection and closed under finite union. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion iscldtop 
|- ( K e. ( Clsd " ( TopOn ` B ) ) <-> ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) )

Proof

Step Hyp Ref Expression
1 fncld 
 |-  Clsd Fn Top
2 fnfun 
 |-  ( Clsd Fn Top -> Fun Clsd )
3 1 2 ax-mp 
 |-  Fun Clsd
4 fvelima 
 |-  ( ( Fun Clsd /\ K e. ( Clsd " ( TopOn ` B ) ) ) -> E. a e. ( TopOn ` B ) ( Clsd ` a ) = K )
5 3 4 mpan 
 |-  ( K e. ( Clsd " ( TopOn ` B ) ) -> E. a e. ( TopOn ` B ) ( Clsd ` a ) = K )
6 cldmreon 
 |-  ( a e. ( TopOn ` B ) -> ( Clsd ` a ) e. ( Moore ` B ) )
7 topontop 
 |-  ( a e. ( TopOn ` B ) -> a e. Top )
8 0cld 
 |-  ( a e. Top -> (/) e. ( Clsd ` a ) )
9 7 8 syl 
 |-  ( a e. ( TopOn ` B ) -> (/) e. ( Clsd ` a ) )
10 uncld 
 |-  ( ( x e. ( Clsd ` a ) /\ y e. ( Clsd ` a ) ) -> ( x u. y ) e. ( Clsd ` a ) )
11 10 adantl 
 |-  ( ( a e. ( TopOn ` B ) /\ ( x e. ( Clsd ` a ) /\ y e. ( Clsd ` a ) ) ) -> ( x u. y ) e. ( Clsd ` a ) )
12 11 ralrimivva 
 |-  ( a e. ( TopOn ` B ) -> A. x e. ( Clsd ` a ) A. y e. ( Clsd ` a ) ( x u. y ) e. ( Clsd ` a ) )
13 6 9 12 3jca 
 |-  ( a e. ( TopOn ` B ) -> ( ( Clsd ` a ) e. ( Moore ` B ) /\ (/) e. ( Clsd ` a ) /\ A. x e. ( Clsd ` a ) A. y e. ( Clsd ` a ) ( x u. y ) e. ( Clsd ` a ) ) )
14 eleq1 
 |-  ( ( Clsd ` a ) = K -> ( ( Clsd ` a ) e. ( Moore ` B ) <-> K e. ( Moore ` B ) ) )
15 eleq2 
 |-  ( ( Clsd ` a ) = K -> ( (/) e. ( Clsd ` a ) <-> (/) e. K ) )
16 eleq2 
 |-  ( ( Clsd ` a ) = K -> ( ( x u. y ) e. ( Clsd ` a ) <-> ( x u. y ) e. K ) )
17 16 raleqbi1dv 
 |-  ( ( Clsd ` a ) = K -> ( A. y e. ( Clsd ` a ) ( x u. y ) e. ( Clsd ` a ) <-> A. y e. K ( x u. y ) e. K ) )
18 17 raleqbi1dv 
 |-  ( ( Clsd ` a ) = K -> ( A. x e. ( Clsd ` a ) A. y e. ( Clsd ` a ) ( x u. y ) e. ( Clsd ` a ) <-> A. x e. K A. y e. K ( x u. y ) e. K ) )
19 14 15 18 3anbi123d 
 |-  ( ( Clsd ` a ) = K -> ( ( ( Clsd ` a ) e. ( Moore ` B ) /\ (/) e. ( Clsd ` a ) /\ A. x e. ( Clsd ` a ) A. y e. ( Clsd ` a ) ( x u. y ) e. ( Clsd ` a ) ) <-> ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) ) )
20 13 19 syl5ibcom 
 |-  ( a e. ( TopOn ` B ) -> ( ( Clsd ` a ) = K -> ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) ) )
21 20 rexlimiv 
 |-  ( E. a e. ( TopOn ` B ) ( Clsd ` a ) = K -> ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) )
22 5 21 syl 
 |-  ( K e. ( Clsd " ( TopOn ` B ) ) -> ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) )
23 simp1 
 |-  ( ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) -> K e. ( Moore ` B ) )
24 simp2 
 |-  ( ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) -> (/) e. K )
25 uneq1 
 |-  ( x = b -> ( x u. y ) = ( b u. y ) )
26 25 eleq1d 
 |-  ( x = b -> ( ( x u. y ) e. K <-> ( b u. y ) e. K ) )
27 uneq2 
 |-  ( y = c -> ( b u. y ) = ( b u. c ) )
28 27 eleq1d 
 |-  ( y = c -> ( ( b u. y ) e. K <-> ( b u. c ) e. K ) )
29 26 28 rspc2v 
 |-  ( ( b e. K /\ c e. K ) -> ( A. x e. K A. y e. K ( x u. y ) e. K -> ( b u. c ) e. K ) )
30 29 com12 
 |-  ( A. x e. K A. y e. K ( x u. y ) e. K -> ( ( b e. K /\ c e. K ) -> ( b u. c ) e. K ) )
31 30 3ad2ant3 
 |-  ( ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) -> ( ( b e. K /\ c e. K ) -> ( b u. c ) e. K ) )
32 31 3impib 
 |-  ( ( ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) /\ b e. K /\ c e. K ) -> ( b u. c ) e. K )
33 eqid 
 |-  { a e. ~P B | ( B \ a ) e. K } = { a e. ~P B | ( B \ a ) e. K }
34 23 24 32 33 mretopd 
 |-  ( ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) -> ( { a e. ~P B | ( B \ a ) e. K } e. ( TopOn ` B ) /\ K = ( Clsd ` { a e. ~P B | ( B \ a ) e. K } ) ) )
35 34 simprd 
 |-  ( ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) -> K = ( Clsd ` { a e. ~P B | ( B \ a ) e. K } ) )
36 34 simpld 
 |-  ( ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) -> { a e. ~P B | ( B \ a ) e. K } e. ( TopOn ` B ) )
37 7 ssriv 
 |-  ( TopOn ` B ) C_ Top
38 1 fndmi 
 |-  dom Clsd = Top
39 37 38 sseqtrri 
 |-  ( TopOn ` B ) C_ dom Clsd
40 funfvima2 
 |-  ( ( Fun Clsd /\ ( TopOn ` B ) C_ dom Clsd ) -> ( { a e. ~P B | ( B \ a ) e. K } e. ( TopOn ` B ) -> ( Clsd ` { a e. ~P B | ( B \ a ) e. K } ) e. ( Clsd " ( TopOn ` B ) ) ) )
41 3 39 40 mp2an 
 |-  ( { a e. ~P B | ( B \ a ) e. K } e. ( TopOn ` B ) -> ( Clsd ` { a e. ~P B | ( B \ a ) e. K } ) e. ( Clsd " ( TopOn ` B ) ) )
42 36 41 syl 
 |-  ( ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) -> ( Clsd ` { a e. ~P B | ( B \ a ) e. K } ) e. ( Clsd " ( TopOn ` B ) ) )
43 35 42 eqeltrd 
 |-  ( ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) -> K e. ( Clsd " ( TopOn ` B ) ) )
44 22 43 impbii 
 |-  ( K e. ( Clsd " ( TopOn ` B ) ) <-> ( K e. ( Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) )