Metamath Proof Explorer

Theorem epttop

Description: The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 ssrab 
 |-  ( y C_ { x e. ~P A | ( P e. x -> x = A ) } <-> ( y C_ ~P A /\ A. x e. y ( P e. x -> x = A ) ) )
2 eleq2 
 |-  ( x = U. y -> ( P e. x <-> P e. U. y ) )
3 eqeq1 
 |-  ( x = U. y -> ( x = A <-> U. y = A ) )
4 2 3 imbi12d 
 |-  ( x = U. y -> ( ( P e. x -> x = A ) <-> ( P e. U. y -> U. y = A ) ) )
5 simprl 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x -> x = A ) ) ) -> y C_ ~P A )
6 sspwuni 
 |-  ( y C_ ~P A <-> U. y C_ A )
7 5 6 sylib 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x -> x = A ) ) ) -> U. y C_ A )
8 vuniex 
 |-  U. y e. _V
9 8 elpw 
 |-  ( U. y e. ~P A <-> U. y C_ A )
10 7 9 sylibr 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x -> x = A ) ) ) -> U. y e. ~P A )
11 eluni2 
 |-  ( P e. U. y <-> E. x e. y P e. x )
12 r19.29 
 |-  ( ( A. x e. y ( P e. x -> x = A ) /\ E. x e. y P e. x ) -> E. x e. y ( ( P e. x -> x = A ) /\ P e. x ) )
13 simpr 
 |-  ( ( x e. y /\ ( P e. x -> x = A ) ) -> ( P e. x -> x = A ) )
14 13 impr 
 |-  ( ( x e. y /\ ( ( P e. x -> x = A ) /\ P e. x ) ) -> x = A )
15 elssuni 
 |-  ( x e. y -> x C_ U. y )
16 15 adantr 
 |-  ( ( x e. y /\ ( ( P e. x -> x = A ) /\ P e. x ) ) -> x C_ U. y )
17 14 16 eqsstrrd 
 |-  ( ( x e. y /\ ( ( P e. x -> x = A ) /\ P e. x ) ) -> A C_ U. y )
18 17 rexlimiva 
 |-  ( E. x e. y ( ( P e. x -> x = A ) /\ P e. x ) -> A C_ U. y )
19 12 18 syl 
 |-  ( ( A. x e. y ( P e. x -> x = A ) /\ E. x e. y P e. x ) -> A C_ U. y )
20 19 ex 
 |-  ( A. x e. y ( P e. x -> x = A ) -> ( E. x e. y P e. x -> A C_ U. y ) )
21 20 ad2antll 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x -> x = A ) ) ) -> ( E. x e. y P e. x -> A C_ U. y ) )
22 11 21 biimtrid 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x -> x = A ) ) ) -> ( P e. U. y -> A C_ U. y ) )
23 22 7 jctild 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x -> x = A ) ) ) -> ( P e. U. y -> ( U. y C_ A /\ A C_ U. y ) ) )
24 eqss 
 |-  ( U. y = A <-> ( U. y C_ A /\ A C_ U. y ) )
25 23 24 imbitrrdi 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x -> x = A ) ) ) -> ( P e. U. y -> U. y = A ) )
26 4 10 25 elrabd 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x -> x = A ) ) ) -> U. y e. { x e. ~P A | ( P e. x -> x = A ) } )
27 26 ex 
 |-  ( ( A e. V /\ P e. A ) -> ( ( y C_ ~P A /\ A. x e. y ( P e. x -> x = A ) ) -> U. y e. { x e. ~P A | ( P e. x -> x = A ) } ) )
28 1 27 biimtrid 
 |-  ( ( A e. V /\ P e. A ) -> ( y C_ { x e. ~P A | ( P e. x -> x = A ) } -> U. y e. { x e. ~P A | ( P e. x -> x = A ) } ) )
29 28 alrimiv 
 |-  ( ( A e. V /\ P e. A ) -> A. y ( y C_ { x e. ~P A | ( P e. x -> x = A ) } -> U. y e. { x e. ~P A | ( P e. x -> x = A ) } ) )
30 inss1 
 |-  ( y i^i z ) C_ y
31 simprll 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) ) -> y e. ~P A )
32 31 elpwid 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) ) -> y C_ A )
33 30 32 sstrid 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) ) -> ( y i^i z ) C_ A )
34 vex 
 |-  y e. _V
35 34 inex1 
 |-  ( y i^i z ) e. _V
36 35 elpw 
 |-  ( ( y i^i z ) e. ~P A <-> ( y i^i z ) C_ A )
37 33 36 sylibr 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) ) -> ( y i^i z ) e. ~P A )
38 elin 
 |-  ( P e. ( y i^i z ) <-> ( P e. y /\ P e. z ) )
39 simprlr 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) ) -> ( P e. y -> y = A ) )
40 simprrr 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) ) -> ( P e. z -> z = A ) )
41 39 40 anim12d 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) ) -> ( ( P e. y /\ P e. z ) -> ( y = A /\ z = A ) ) )
42 ineq12 
 |-  ( ( y = A /\ z = A ) -> ( y i^i z ) = ( A i^i A ) )
43 inidm 
 |-  ( A i^i A ) = A
44 42 43 eqtrdi 
 |-  ( ( y = A /\ z = A ) -> ( y i^i z ) = A )
45 41 44 syl6 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) ) -> ( ( P e. y /\ P e. z ) -> ( y i^i z ) = A ) )
46 38 45 biimtrid 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) ) -> ( P e. ( y i^i z ) -> ( y i^i z ) = A ) )
47 37 46 jca 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) ) -> ( ( y i^i z ) e. ~P A /\ ( P e. ( y i^i z ) -> ( y i^i z ) = A ) ) )
48 47 ex 
 |-  ( ( A e. V /\ P e. A ) -> ( ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) -> ( ( y i^i z ) e. ~P A /\ ( P e. ( y i^i z ) -> ( y i^i z ) = A ) ) ) )
49 eleq2 
 |-  ( x = y -> ( P e. x <-> P e. y ) )
50 eqeq1 
 |-  ( x = y -> ( x = A <-> y = A ) )
51 49 50 imbi12d 
 |-  ( x = y -> ( ( P e. x -> x = A ) <-> ( P e. y -> y = A ) ) )
52 51 elrab 
 |-  ( y e. { x e. ~P A | ( P e. x -> x = A ) } <-> ( y e. ~P A /\ ( P e. y -> y = A ) ) )
53 eleq2 
 |-  ( x = z -> ( P e. x <-> P e. z ) )
54 eqeq1 
 |-  ( x = z -> ( x = A <-> z = A ) )
55 53 54 imbi12d 
 |-  ( x = z -> ( ( P e. x -> x = A ) <-> ( P e. z -> z = A ) ) )
56 55 elrab 
 |-  ( z e. { x e. ~P A | ( P e. x -> x = A ) } <-> ( z e. ~P A /\ ( P e. z -> z = A ) ) )
57 52 56 anbi12i 
 |-  ( ( y e. { x e. ~P A | ( P e. x -> x = A ) } /\ z e. { x e. ~P A | ( P e. x -> x = A ) } ) <-> ( ( y e. ~P A /\ ( P e. y -> y = A ) ) /\ ( z e. ~P A /\ ( P e. z -> z = A ) ) ) )
58 eleq2 
 |-  ( x = ( y i^i z ) -> ( P e. x <-> P e. ( y i^i z ) ) )
59 eqeq1 
 |-  ( x = ( y i^i z ) -> ( x = A <-> ( y i^i z ) = A ) )
60 58 59 imbi12d 
 |-  ( x = ( y i^i z ) -> ( ( P e. x -> x = A ) <-> ( P e. ( y i^i z ) -> ( y i^i z ) = A ) ) )
61 60 elrab 
 |-  ( ( y i^i z ) e. { x e. ~P A | ( P e. x -> x = A ) } <-> ( ( y i^i z ) e. ~P A /\ ( P e. ( y i^i z ) -> ( y i^i z ) = A ) ) )
62 48 57 61 3imtr4g 
 |-  ( ( A e. V /\ P e. A ) -> ( ( y e. { x e. ~P A | ( P e. x -> x = A ) } /\ z e. { x e. ~P A | ( P e. x -> x = A ) } ) -> ( y i^i z ) e. { x e. ~P A | ( P e. x -> x = A ) } ) )
63 62 ralrimivv 
 |-  ( ( A e. V /\ P e. A ) -> A. y e. { x e. ~P A | ( P e. x -> x = A ) } A. z e. { x e. ~P A | ( P e. x -> x = A ) } ( y i^i z ) e. { x e. ~P A | ( P e. x -> x = A ) } )
64 pwexg 
 |-  ( A e. V -> ~P A e. _V )
65 64 adantr 
 |-  ( ( A e. V /\ P e. A ) -> ~P A e. _V )
66 rabexg 
 |-  ( ~P A e. _V -> { x e. ~P A | ( P e. x -> x = A ) } e. _V )
67 65 66 syl 
 |-  ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x -> x = A ) } e. _V )
68 istopg 
 |-  ( { x e. ~P A | ( P e. x -> x = A ) } e. _V -> ( { x e. ~P A | ( P e. x -> x = A ) } e. Top <-> ( A. y ( y C_ { x e. ~P A | ( P e. x -> x = A ) } -> U. y e. { x e. ~P A | ( P e. x -> x = A ) } ) /\ A. y e. { x e. ~P A | ( P e. x -> x = A ) } A. z e. { x e. ~P A | ( P e. x -> x = A ) } ( y i^i z ) e. { x e. ~P A | ( P e. x -> x = A ) } ) ) )
69 67 68 syl 
 |-  ( ( A e. V /\ P e. A ) -> ( { x e. ~P A | ( P e. x -> x = A ) } e. Top <-> ( A. y ( y C_ { x e. ~P A | ( P e. x -> x = A ) } -> U. y e. { x e. ~P A | ( P e. x -> x = A ) } ) /\ A. y e. { x e. ~P A | ( P e. x -> x = A ) } A. z e. { x e. ~P A | ( P e. x -> x = A ) } ( y i^i z ) e. { x e. ~P A | ( P e. x -> x = A ) } ) ) )
70 29 63 69 mpbir2and 
 |-  ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x -> x = A ) } e. Top )
71 eleq2 
 |-  ( x = A -> ( P e. x <-> P e. A ) )
72 eqeq1 
 |-  ( x = A -> ( x = A <-> A = A ) )
73 71 72 imbi12d 
 |-  ( x = A -> ( ( P e. x -> x = A ) <-> ( P e. A -> A = A ) ) )
74 pwidg 
 |-  ( A e. V -> A e. ~P A )
75 74 adantr 
 |-  ( ( A e. V /\ P e. A ) -> A e. ~P A )
76 eqidd 
 |-  ( ( A e. V /\ P e. A ) -> A = A )
77 76 a1d 
 |-  ( ( A e. V /\ P e. A ) -> ( P e. A -> A = A ) )
78 73 75 77 elrabd 
 |-  ( ( A e. V /\ P e. A ) -> A e. { x e. ~P A | ( P e. x -> x = A ) } )
79 elssuni 
 |-  ( A e. { x e. ~P A | ( P e. x -> x = A ) } -> A C_ U. { x e. ~P A | ( P e. x -> x = A ) } )
80 78 79 syl 
 |-  ( ( A e. V /\ P e. A ) -> A C_ U. { x e. ~P A | ( P e. x -> x = A ) } )
81 ssrab2 
 |-  { x e. ~P A | ( P e. x -> x = A ) } C_ ~P A
82 sspwuni 
 |-  ( { x e. ~P A | ( P e. x -> x = A ) } C_ ~P A <-> U. { x e. ~P A | ( P e. x -> x = A ) } C_ A )
83 81 82 mpbi 
 |-  U. { x e. ~P A | ( P e. x -> x = A ) } C_ A
84 83 a1i 
 |-  ( ( A e. V /\ P e. A ) -> U. { x e. ~P A | ( P e. x -> x = A ) } C_ A )
85 80 84 eqssd 
 |-  ( ( A e. V /\ P e. A ) -> A = U. { x e. ~P A | ( P e. x -> x = A ) } )
86 istopon 
 |-  ( { x e. ~P A | ( P e. x -> x = A ) } e. ( TopOn ` A ) <-> ( { x e. ~P A | ( P e. x -> x = A ) } e. Top /\ A = U. { x e. ~P A | ( P e. x -> x = A ) } ) )
87 70 85 86 sylanbrc 
 |-  ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x -> x = A ) } e. ( TopOn ` A ) )