Metamath Proof Explorer

Theorem cctop

Description: The countable complement topology on a set A . Example 4 in Munkres p. 77. (Contributed by FL, 23-Aug-2006) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion cctop 
|- ( A e. V -> { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } e. ( TopOn ` A ) )

Proof

Step Hyp Ref Expression
1 difeq2 
 |-  ( x = U. y -> ( A \ x ) = ( A \ U. y ) )
2 1 breq1d 
 |-  ( x = U. y -> ( ( A \ x ) ~<_ _om <-> ( A \ U. y ) ~<_ _om ) )
3 eqeq1 
 |-  ( x = U. y -> ( x = (/) <-> U. y = (/) ) )
4 2 3 orbi12d 
 |-  ( x = U. y -> ( ( ( A \ x ) ~<_ _om \/ x = (/) ) <-> ( ( A \ U. y ) ~<_ _om \/ U. y = (/) ) ) )
5 uniss 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> U. y C_ U. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } )
6 ssrab2 
 |-  { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } C_ ~P A
7 sspwuni 
 |-  ( { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } C_ ~P A <-> U. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } C_ A )
8 6 7 mpbi 
 |-  U. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } C_ A
9 5 8 sstrdi 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> U. y C_ A )
10 vuniex 
 |-  U. y e. _V
11 10 elpw 
 |-  ( U. y e. ~P A <-> U. y C_ A )
12 9 11 sylibr 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> U. y e. ~P A )
13 uni0c 
 |-  ( U. y = (/) <-> A. z e. y z = (/) )
14 13 notbii 
 |-  ( -. U. y = (/) <-> -. A. z e. y z = (/) )
15 rexnal 
 |-  ( E. z e. y -. z = (/) <-> -. A. z e. y z = (/) )
16 14 15 bitr4i 
 |-  ( -. U. y = (/) <-> E. z e. y -. z = (/) )
17 ssel2 
 |-  ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) -> z e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } )
18 difeq2 
 |-  ( x = z -> ( A \ x ) = ( A \ z ) )
19 18 breq1d 
 |-  ( x = z -> ( ( A \ x ) ~<_ _om <-> ( A \ z ) ~<_ _om ) )
20 eqeq1 
 |-  ( x = z -> ( x = (/) <-> z = (/) ) )
21 19 20 orbi12d 
 |-  ( x = z -> ( ( ( A \ x ) ~<_ _om \/ x = (/) ) <-> ( ( A \ z ) ~<_ _om \/ z = (/) ) ) )
22 21 elrab 
 |-  ( z e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } <-> ( z e. ~P A /\ ( ( A \ z ) ~<_ _om \/ z = (/) ) ) )
23 17 22 sylib 
 |-  ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) -> ( z e. ~P A /\ ( ( A \ z ) ~<_ _om \/ z = (/) ) ) )
24 23 simprd 
 |-  ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) -> ( ( A \ z ) ~<_ _om \/ z = (/) ) )
25 24 ord 
 |-  ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) -> ( -. ( A \ z ) ~<_ _om -> z = (/) ) )
26 25 con1d 
 |-  ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) -> ( -. z = (/) -> ( A \ z ) ~<_ _om ) )
27 26 imp 
 |-  ( ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) /\ -. z = (/) ) -> ( A \ z ) ~<_ _om )
28 ctex 
 |-  ( ( A \ z ) ~<_ _om -> ( A \ z ) e. _V )
29 28 adantl 
 |-  ( ( ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) /\ -. z = (/) ) /\ ( A \ z ) ~<_ _om ) -> ( A \ z ) e. _V )
30 simpllr 
 |-  ( ( ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) /\ -. z = (/) ) /\ ( A \ z ) ~<_ _om ) -> z e. y )
31 elssuni 
 |-  ( z e. y -> z C_ U. y )
32 sscon 
 |-  ( z C_ U. y -> ( A \ U. y ) C_ ( A \ z ) )
33 30 31 32 3syl 
 |-  ( ( ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) /\ -. z = (/) ) /\ ( A \ z ) ~<_ _om ) -> ( A \ U. y ) C_ ( A \ z ) )
34 ssdomg 
 |-  ( ( A \ z ) e. _V -> ( ( A \ U. y ) C_ ( A \ z ) -> ( A \ U. y ) ~<_ ( A \ z ) ) )
35 29 33 34 sylc 
 |-  ( ( ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) /\ -. z = (/) ) /\ ( A \ z ) ~<_ _om ) -> ( A \ U. y ) ~<_ ( A \ z ) )
36 domtr 
 |-  ( ( ( A \ U. y ) ~<_ ( A \ z ) /\ ( A \ z ) ~<_ _om ) -> ( A \ U. y ) ~<_ _om )
37 35 36 sylancom 
 |-  ( ( ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) /\ -. z = (/) ) /\ ( A \ z ) ~<_ _om ) -> ( A \ U. y ) ~<_ _om )
38 27 37 mpdan 
 |-  ( ( ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. y ) /\ -. z = (/) ) -> ( A \ U. y ) ~<_ _om )
39 38 rexlimdva2 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> ( E. z e. y -. z = (/) -> ( A \ U. y ) ~<_ _om ) )
40 16 39 syl5bi 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> ( -. U. y = (/) -> ( A \ U. y ) ~<_ _om ) )
41 40 con1d 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> ( -. ( A \ U. y ) ~<_ _om -> U. y = (/) ) )
42 41 orrd 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> ( ( A \ U. y ) ~<_ _om \/ U. y = (/) ) )
43 4 12 42 elrabd 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> U. y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } )
44 43 ax-gen 
 |-  A. y ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> U. y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } )
45 difeq2 
 |-  ( x = y -> ( A \ x ) = ( A \ y ) )
46 45 breq1d 
 |-  ( x = y -> ( ( A \ x ) ~<_ _om <-> ( A \ y ) ~<_ _om ) )
47 eqeq1 
 |-  ( x = y -> ( x = (/) <-> y = (/) ) )
48 46 47 orbi12d 
 |-  ( x = y -> ( ( ( A \ x ) ~<_ _om \/ x = (/) ) <-> ( ( A \ y ) ~<_ _om \/ y = (/) ) ) )
49 48 elrab 
 |-  ( y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } <-> ( y e. ~P A /\ ( ( A \ y ) ~<_ _om \/ y = (/) ) ) )
50 ssinss1 
 |-  ( y C_ A -> ( y i^i z ) C_ A )
51 vex 
 |-  y e. _V
52 51 elpw 
 |-  ( y e. ~P A <-> y C_ A )
53 51 inex1 
 |-  ( y i^i z ) e. _V
54 53 elpw 
 |-  ( ( y i^i z ) e. ~P A <-> ( y i^i z ) C_ A )
55 50 52 54 3imtr4i 
 |-  ( y e. ~P A -> ( y i^i z ) e. ~P A )
56 55 ad2antrr 
 |-  ( ( ( y e. ~P A /\ ( ( A \ y ) ~<_ _om \/ y = (/) ) ) /\ ( z e. ~P A /\ ( ( A \ z ) ~<_ _om \/ z = (/) ) ) ) -> ( y i^i z ) e. ~P A )
57 difindi 
 |-  ( A \ ( y i^i z ) ) = ( ( A \ y ) u. ( A \ z ) )
58 unctb 
 |-  ( ( ( A \ y ) ~<_ _om /\ ( A \ z ) ~<_ _om ) -> ( ( A \ y ) u. ( A \ z ) ) ~<_ _om )
59 57 58 eqbrtrid 
 |-  ( ( ( A \ y ) ~<_ _om /\ ( A \ z ) ~<_ _om ) -> ( A \ ( y i^i z ) ) ~<_ _om )
60 59 orcd 
 |-  ( ( ( A \ y ) ~<_ _om /\ ( A \ z ) ~<_ _om ) -> ( ( A \ ( y i^i z ) ) ~<_ _om \/ ( y i^i z ) = (/) ) )
61 ineq1 
 |-  ( y = (/) -> ( y i^i z ) = ( (/) i^i z ) )
62 0in 
 |-  ( (/) i^i z ) = (/)
63 61 62 eqtrdi 
 |-  ( y = (/) -> ( y i^i z ) = (/) )
64 63 olcd 
 |-  ( y = (/) -> ( ( A \ ( y i^i z ) ) ~<_ _om \/ ( y i^i z ) = (/) ) )
65 ineq2 
 |-  ( z = (/) -> ( y i^i z ) = ( y i^i (/) ) )
66 in0 
 |-  ( y i^i (/) ) = (/)
67 65 66 eqtrdi 
 |-  ( z = (/) -> ( y i^i z ) = (/) )
68 67 olcd 
 |-  ( z = (/) -> ( ( A \ ( y i^i z ) ) ~<_ _om \/ ( y i^i z ) = (/) ) )
69 60 64 68 ccase2 
 |-  ( ( ( ( A \ y ) ~<_ _om \/ y = (/) ) /\ ( ( A \ z ) ~<_ _om \/ z = (/) ) ) -> ( ( A \ ( y i^i z ) ) ~<_ _om \/ ( y i^i z ) = (/) ) )
70 69 ad2ant2l 
 |-  ( ( ( y e. ~P A /\ ( ( A \ y ) ~<_ _om \/ y = (/) ) ) /\ ( z e. ~P A /\ ( ( A \ z ) ~<_ _om \/ z = (/) ) ) ) -> ( ( A \ ( y i^i z ) ) ~<_ _om \/ ( y i^i z ) = (/) ) )
71 56 70 jca 
 |-  ( ( ( y e. ~P A /\ ( ( A \ y ) ~<_ _om \/ y = (/) ) ) /\ ( z e. ~P A /\ ( ( A \ z ) ~<_ _om \/ z = (/) ) ) ) -> ( ( y i^i z ) e. ~P A /\ ( ( A \ ( y i^i z ) ) ~<_ _om \/ ( y i^i z ) = (/) ) ) )
72 49 22 71 syl2anb 
 |-  ( ( y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ) -> ( ( y i^i z ) e. ~P A /\ ( ( A \ ( y i^i z ) ) ~<_ _om \/ ( y i^i z ) = (/) ) ) )
73 difeq2 
 |-  ( x = ( y i^i z ) -> ( A \ x ) = ( A \ ( y i^i z ) ) )
74 73 breq1d 
 |-  ( x = ( y i^i z ) -> ( ( A \ x ) ~<_ _om <-> ( A \ ( y i^i z ) ) ~<_ _om ) )
75 eqeq1 
 |-  ( x = ( y i^i z ) -> ( x = (/) <-> ( y i^i z ) = (/) ) )
76 74 75 orbi12d 
 |-  ( x = ( y i^i z ) -> ( ( ( A \ x ) ~<_ _om \/ x = (/) ) <-> ( ( A \ ( y i^i z ) ) ~<_ _om \/ ( y i^i z ) = (/) ) ) )
77 76 elrab 
 |-  ( ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } <-> ( ( y i^i z ) e. ~P A /\ ( ( A \ ( y i^i z ) ) ~<_ _om \/ ( y i^i z ) = (/) ) ) )
78 72 77 sylibr 
 |-  ( ( y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } /\ z e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ) -> ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } )
79 78 rgen2 
 |-  A. y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } A. z e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) }
80 44 79 pm3.2i 
 |-  ( A. y ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> U. y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ) /\ A. y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } A. z e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } )
81 pwexg 
 |-  ( A e. V -> ~P A e. _V )
82 rabexg 
 |-  ( ~P A e. _V -> { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } e. _V )
83 istopg 
 |-  ( { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } e. _V -> ( { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } e. Top <-> ( A. y ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> U. y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ) /\ A. y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } A. z e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ) ) )
84 81 82 83 3syl 
 |-  ( A e. V -> ( { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } e. Top <-> ( A. y ( y C_ { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> U. y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ) /\ A. y e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } A. z e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ) ) )
85 80 84 mpbiri 
 |-  ( A e. V -> { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } e. Top )
86 difeq2 
 |-  ( x = A -> ( A \ x ) = ( A \ A ) )
87 difid 
 |-  ( A \ A ) = (/)
88 86 87 eqtrdi 
 |-  ( x = A -> ( A \ x ) = (/) )
89 88 breq1d 
 |-  ( x = A -> ( ( A \ x ) ~<_ _om <-> (/) ~<_ _om ) )
90 eqeq1 
 |-  ( x = A -> ( x = (/) <-> A = (/) ) )
91 89 90 orbi12d 
 |-  ( x = A -> ( ( ( A \ x ) ~<_ _om \/ x = (/) ) <-> ( (/) ~<_ _om \/ A = (/) ) ) )
92 pwidg 
 |-  ( A e. V -> A e. ~P A )
93 omex 
 |-  _om e. _V
94 93 0dom 
 |-  (/) ~<_ _om
95 94 orci 
 |-  ( (/) ~<_ _om \/ A = (/) )
96 95 a1i 
 |-  ( A e. V -> ( (/) ~<_ _om \/ A = (/) ) )
97 91 92 96 elrabd 
 |-  ( A e. V -> A e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } )
98 elssuni 
 |-  ( A e. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } -> A C_ U. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } )
99 97 98 syl 
 |-  ( A e. V -> A C_ U. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } )
100 8 a1i 
 |-  ( A e. V -> U. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } C_ A )
101 99 100 eqssd 
 |-  ( A e. V -> A = U. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } )
102 istopon 
 |-  ( { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } e. ( TopOn ` A ) <-> ( { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } e. Top /\ A = U. { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } ) )
103 85 101 102 sylanbrc 
 |-  ( A e. V -> { x e. ~P A | ( ( A \ x ) ~<_ _om \/ x = (/) ) } e. ( TopOn ` A ) )