Metamath Proof Explorer

Theorem fctop

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

Ref Expression
Assertion fctop 
|- ( A e. V -> { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. ( TopOn ` A ) )

Proof

Step Hyp Ref Expression
1 difeq2 
 |-  ( x = U. y -> ( A \ x ) = ( A \ U. y ) )
2 1 eleq1d 
 |-  ( x = U. y -> ( ( A \ x ) e. Fin <-> ( A \ U. y ) e. Fin ) )
3 eqeq1 
 |-  ( x = U. y -> ( x = (/) <-> U. y = (/) ) )
4 2 3 orbi12d 
 |-  ( x = U. y -> ( ( ( A \ x ) e. Fin \/ x = (/) ) <-> ( ( A \ U. y ) e. Fin \/ U. y = (/) ) ) )
5 uniss 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> U. y C_ U. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } )
6 ssrab2 
 |-  { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } C_ ~P A
7 sspwuni 
 |-  ( { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } C_ ~P A <-> U. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } C_ A )
8 6 7 mpbi 
 |-  U. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } C_ A
9 5 8 sstrdi 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ 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 ) e. Fin \/ 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 ) e. Fin \/ x = (/) ) } /\ z e. y ) -> z e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } )
18 difeq2 
 |-  ( x = z -> ( A \ x ) = ( A \ z ) )
19 18 eleq1d 
 |-  ( x = z -> ( ( A \ x ) e. Fin <-> ( A \ z ) e. Fin ) )
20 eqeq1 
 |-  ( x = z -> ( x = (/) <-> z = (/) ) )
21 19 20 orbi12d 
 |-  ( x = z -> ( ( ( A \ x ) e. Fin \/ x = (/) ) <-> ( ( A \ z ) e. Fin \/ z = (/) ) ) )
22 21 elrab 
 |-  ( z e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } <-> ( z e. ~P A /\ ( ( A \ z ) e. Fin \/ z = (/) ) ) )
23 17 22 sylib 
 |-  ( ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } /\ z e. y ) -> ( z e. ~P A /\ ( ( A \ z ) e. Fin \/ z = (/) ) ) )
24 23 simprd 
 |-  ( ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } /\ z e. y ) -> ( ( A \ z ) e. Fin \/ z = (/) ) )
25 24 ord 
 |-  ( ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } /\ z e. y ) -> ( -. ( A \ z ) e. Fin -> z = (/) ) )
26 25 con1d 
 |-  ( ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } /\ z e. y ) -> ( -. z = (/) -> ( A \ z ) e. Fin ) )
27 26 imp 
 |-  ( ( ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } /\ z e. y ) /\ -. z = (/) ) -> ( A \ z ) e. Fin )
28 elssuni 
 |-  ( z e. y -> z C_ U. y )
29 28 sscond 
 |-  ( z e. y -> ( A \ U. y ) C_ ( A \ z ) )
30 ssfi 
 |-  ( ( ( A \ z ) e. Fin /\ ( A \ U. y ) C_ ( A \ z ) ) -> ( A \ U. y ) e. Fin )
31 29 30 sylan2 
 |-  ( ( ( A \ z ) e. Fin /\ z e. y ) -> ( A \ U. y ) e. Fin )
32 31 expcom 
 |-  ( z e. y -> ( ( A \ z ) e. Fin -> ( A \ U. y ) e. Fin ) )
33 32 ad2antlr 
 |-  ( ( ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } /\ z e. y ) /\ -. z = (/) ) -> ( ( A \ z ) e. Fin -> ( A \ U. y ) e. Fin ) )
34 27 33 mpd 
 |-  ( ( ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } /\ z e. y ) /\ -. z = (/) ) -> ( A \ U. y ) e. Fin )
35 34 rexlimdva2 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> ( E. z e. y -. z = (/) -> ( A \ U. y ) e. Fin ) )
36 16 35 biimtrid 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> ( -. U. y = (/) -> ( A \ U. y ) e. Fin ) )
37 36 con1d 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> ( -. ( A \ U. y ) e. Fin -> U. y = (/) ) )
38 37 orrd 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> ( ( A \ U. y ) e. Fin \/ U. y = (/) ) )
39 4 12 38 elrabd 
 |-  ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> U. y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } )
40 39 ax-gen 
 |-  A. y ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> U. y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } )
41 ssinss1 
 |-  ( y C_ A -> ( y i^i z ) C_ A )
42 vex 
 |-  y e. _V
43 42 elpw 
 |-  ( y e. ~P A <-> y C_ A )
44 42 inex1 
 |-  ( y i^i z ) e. _V
45 44 elpw 
 |-  ( ( y i^i z ) e. ~P A <-> ( y i^i z ) C_ A )
46 41 43 45 3imtr4i 
 |-  ( y e. ~P A -> ( y i^i z ) e. ~P A )
47 46 ad2antrr 
 |-  ( ( ( y e. ~P A /\ ( ( A \ y ) e. Fin \/ y = (/) ) ) /\ ( z e. ~P A /\ ( ( A \ z ) e. Fin \/ z = (/) ) ) ) -> ( y i^i z ) e. ~P A )
48 difindi 
 |-  ( A \ ( y i^i z ) ) = ( ( A \ y ) u. ( A \ z ) )
49 unfi 
 |-  ( ( ( A \ y ) e. Fin /\ ( A \ z ) e. Fin ) -> ( ( A \ y ) u. ( A \ z ) ) e. Fin )
50 48 49 eqeltrid 
 |-  ( ( ( A \ y ) e. Fin /\ ( A \ z ) e. Fin ) -> ( A \ ( y i^i z ) ) e. Fin )
51 50 orcd 
 |-  ( ( ( A \ y ) e. Fin /\ ( A \ z ) e. Fin ) -> ( ( A \ ( y i^i z ) ) e. Fin \/ ( y i^i z ) = (/) ) )
52 ineq1 
 |-  ( y = (/) -> ( y i^i z ) = ( (/) i^i z ) )
53 0in 
 |-  ( (/) i^i z ) = (/)
54 52 53 eqtrdi 
 |-  ( y = (/) -> ( y i^i z ) = (/) )
55 54 olcd 
 |-  ( y = (/) -> ( ( A \ ( y i^i z ) ) e. Fin \/ ( y i^i z ) = (/) ) )
56 ineq2 
 |-  ( z = (/) -> ( y i^i z ) = ( y i^i (/) ) )
57 in0 
 |-  ( y i^i (/) ) = (/)
58 56 57 eqtrdi 
 |-  ( z = (/) -> ( y i^i z ) = (/) )
59 58 olcd 
 |-  ( z = (/) -> ( ( A \ ( y i^i z ) ) e. Fin \/ ( y i^i z ) = (/) ) )
60 51 55 59 ccase2 
 |-  ( ( ( ( A \ y ) e. Fin \/ y = (/) ) /\ ( ( A \ z ) e. Fin \/ z = (/) ) ) -> ( ( A \ ( y i^i z ) ) e. Fin \/ ( y i^i z ) = (/) ) )
61 60 ad2ant2l 
 |-  ( ( ( y e. ~P A /\ ( ( A \ y ) e. Fin \/ y = (/) ) ) /\ ( z e. ~P A /\ ( ( A \ z ) e. Fin \/ z = (/) ) ) ) -> ( ( A \ ( y i^i z ) ) e. Fin \/ ( y i^i z ) = (/) ) )
62 47 61 jca 
 |-  ( ( ( y e. ~P A /\ ( ( A \ y ) e. Fin \/ y = (/) ) ) /\ ( z e. ~P A /\ ( ( A \ z ) e. Fin \/ z = (/) ) ) ) -> ( ( y i^i z ) e. ~P A /\ ( ( A \ ( y i^i z ) ) e. Fin \/ ( y i^i z ) = (/) ) ) )
63 difeq2 
 |-  ( x = y -> ( A \ x ) = ( A \ y ) )
64 63 eleq1d 
 |-  ( x = y -> ( ( A \ x ) e. Fin <-> ( A \ y ) e. Fin ) )
65 eqeq1 
 |-  ( x = y -> ( x = (/) <-> y = (/) ) )
66 64 65 orbi12d 
 |-  ( x = y -> ( ( ( A \ x ) e. Fin \/ x = (/) ) <-> ( ( A \ y ) e. Fin \/ y = (/) ) ) )
67 66 elrab 
 |-  ( y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } <-> ( y e. ~P A /\ ( ( A \ y ) e. Fin \/ y = (/) ) ) )
68 67 22 anbi12i 
 |-  ( ( y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } /\ z e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ) <-> ( ( y e. ~P A /\ ( ( A \ y ) e. Fin \/ y = (/) ) ) /\ ( z e. ~P A /\ ( ( A \ z ) e. Fin \/ z = (/) ) ) ) )
69 difeq2 
 |-  ( x = ( y i^i z ) -> ( A \ x ) = ( A \ ( y i^i z ) ) )
70 69 eleq1d 
 |-  ( x = ( y i^i z ) -> ( ( A \ x ) e. Fin <-> ( A \ ( y i^i z ) ) e. Fin ) )
71 eqeq1 
 |-  ( x = ( y i^i z ) -> ( x = (/) <-> ( y i^i z ) = (/) ) )
72 70 71 orbi12d 
 |-  ( x = ( y i^i z ) -> ( ( ( A \ x ) e. Fin \/ x = (/) ) <-> ( ( A \ ( y i^i z ) ) e. Fin \/ ( y i^i z ) = (/) ) ) )
73 72 elrab 
 |-  ( ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } <-> ( ( y i^i z ) e. ~P A /\ ( ( A \ ( y i^i z ) ) e. Fin \/ ( y i^i z ) = (/) ) ) )
74 62 68 73 3imtr4i 
 |-  ( ( y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } /\ z e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ) -> ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } )
75 74 rgen2 
 |-  A. y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } A. z e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) }
76 40 75 pm3.2i 
 |-  ( A. y ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> U. y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ) /\ A. y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } A. z e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } )
77 pwexg 
 |-  ( A e. V -> ~P A e. _V )
78 rabexg 
 |-  ( ~P A e. _V -> { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. _V )
79 istopg 
 |-  ( { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. _V -> ( { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. Top <-> ( A. y ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> U. y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ) /\ A. y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } A. z e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ) ) )
80 77 78 79 3syl 
 |-  ( A e. V -> ( { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. Top <-> ( A. y ( y C_ { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> U. y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ) /\ A. y e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } A. z e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ) ) )
81 76 80 mpbiri 
 |-  ( A e. V -> { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. Top )
82 difeq2 
 |-  ( x = A -> ( A \ x ) = ( A \ A ) )
83 difid 
 |-  ( A \ A ) = (/)
84 82 83 eqtrdi 
 |-  ( x = A -> ( A \ x ) = (/) )
85 84 eleq1d 
 |-  ( x = A -> ( ( A \ x ) e. Fin <-> (/) e. Fin ) )
86 eqeq1 
 |-  ( x = A -> ( x = (/) <-> A = (/) ) )
87 85 86 orbi12d 
 |-  ( x = A -> ( ( ( A \ x ) e. Fin \/ x = (/) ) <-> ( (/) e. Fin \/ A = (/) ) ) )
88 pwidg 
 |-  ( A e. V -> A e. ~P A )
89 0fi 
 |-  (/) e. Fin
90 89 orci 
 |-  ( (/) e. Fin \/ A = (/) )
91 90 a1i 
 |-  ( A e. V -> ( (/) e. Fin \/ A = (/) ) )
92 87 88 91 elrabd 
 |-  ( A e. V -> A e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } )
93 elssuni 
 |-  ( A e. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } -> A C_ U. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } )
94 92 93 syl 
 |-  ( A e. V -> A C_ U. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } )
95 8 a1i 
 |-  ( A e. V -> U. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } C_ A )
96 94 95 eqssd 
 |-  ( A e. V -> A = U. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } )
97 istopon 
 |-  ( { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. ( TopOn ` A ) <-> ( { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. Top /\ A = U. { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } ) )
98 81 96 97 sylanbrc 
 |-  ( A e. V -> { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. ( TopOn ` A ) )