Metamath Proof Explorer

Theorem ppttop

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

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

Proof

Step Hyp Ref Expression
1 ssrab 
 |-  ( y C_ { x e. ~P A | ( P e. x \/ x = (/) ) } <-> ( y C_ ~P A /\ A. x e. y ( P e. x \/ x = (/) ) ) )
2 eleq2 
 |-  ( x = U. y -> ( P e. x <-> P e. U. y ) )
3 eqeq1 
 |-  ( x = U. y -> ( x = (/) <-> U. y = (/) ) )
4 2 3 orbi12d 
 |-  ( x = U. y -> ( ( P e. x \/ x = (/) ) <-> ( P e. U. y \/ U. y = (/) ) ) )
5 simprl 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x \/ x = (/) ) ) ) -> 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 = (/) ) ) ) -> 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 = (/) ) ) ) -> U. y e. ~P A )
11 neq0 
 |-  ( -. U. y = (/) <-> E. z z e. U. y )
12 eluni2 
 |-  ( z e. U. y <-> E. x e. y z e. x )
13 r19.29 
 |-  ( ( A. x e. y ( P e. x \/ x = (/) ) /\ E. x e. y z e. x ) -> E. x e. y ( ( P e. x \/ x = (/) ) /\ z e. x ) )
14 n0i 
 |-  ( z e. x -> -. x = (/) )
15 14 adantl 
 |-  ( ( ( P e. x \/ x = (/) ) /\ z e. x ) -> -. x = (/) )
16 simpl 
 |-  ( ( ( P e. x \/ x = (/) ) /\ z e. x ) -> ( P e. x \/ x = (/) ) )
17 16 ord 
 |-  ( ( ( P e. x \/ x = (/) ) /\ z e. x ) -> ( -. P e. x -> x = (/) ) )
18 15 17 mt3d 
 |-  ( ( ( P e. x \/ x = (/) ) /\ z e. x ) -> P e. x )
19 simpl 
 |-  ( ( x e. y /\ ( ( P e. x \/ x = (/) ) /\ z e. x ) ) -> x e. y )
20 elunii 
 |-  ( ( P e. x /\ x e. y ) -> P e. U. y )
21 18 19 20 syl2an2 
 |-  ( ( x e. y /\ ( ( P e. x \/ x = (/) ) /\ z e. x ) ) -> P e. U. y )
22 21 rexlimiva 
 |-  ( E. x e. y ( ( P e. x \/ x = (/) ) /\ z e. x ) -> P e. U. y )
23 13 22 syl 
 |-  ( ( A. x e. y ( P e. x \/ x = (/) ) /\ E. x e. y z e. x ) -> P e. U. y )
24 23 ex 
 |-  ( A. x e. y ( P e. x \/ x = (/) ) -> ( E. x e. y z e. x -> P e. U. y ) )
25 24 ad2antll 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x \/ x = (/) ) ) ) -> ( E. x e. y z e. x -> P e. U. y ) )
26 12 25 biimtrid 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x \/ x = (/) ) ) ) -> ( z e. U. y -> P e. U. y ) )
27 26 exlimdv 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x \/ x = (/) ) ) ) -> ( E. z z e. U. y -> P e. U. y ) )
28 11 27 biimtrid 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x \/ x = (/) ) ) ) -> ( -. U. y = (/) -> P e. U. y ) )
29 28 con1d 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x \/ x = (/) ) ) ) -> ( -. P e. U. y -> U. y = (/) ) )
30 29 orrd 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x \/ x = (/) ) ) ) -> ( P e. U. y \/ U. y = (/) ) )
31 4 10 30 elrabd 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( y C_ ~P A /\ A. x e. y ( P e. x \/ x = (/) ) ) ) -> U. y e. { x e. ~P A | ( P e. x \/ x = (/) ) } )
32 31 ex 
 |-  ( ( A e. V /\ P e. A ) -> ( ( y C_ ~P A /\ A. x e. y ( P e. x \/ x = (/) ) ) -> U. y e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) )
33 1 32 biimtrid 
 |-  ( ( A e. V /\ P e. A ) -> ( y C_ { x e. ~P A | ( P e. x \/ x = (/) ) } -> U. y e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) )
34 33 alrimiv 
 |-  ( ( A e. V /\ P e. A ) -> A. y ( y C_ { x e. ~P A | ( P e. x \/ x = (/) ) } -> U. y e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) )
35 eleq2 
 |-  ( x = y -> ( P e. x <-> P e. y ) )
36 eqeq1 
 |-  ( x = y -> ( x = (/) <-> y = (/) ) )
37 35 36 orbi12d 
 |-  ( x = y -> ( ( P e. x \/ x = (/) ) <-> ( P e. y \/ y = (/) ) ) )
38 37 elrab 
 |-  ( y e. { x e. ~P A | ( P e. x \/ x = (/) ) } <-> ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) )
39 eleq2 
 |-  ( x = z -> ( P e. x <-> P e. z ) )
40 eqeq1 
 |-  ( x = z -> ( x = (/) <-> z = (/) ) )
41 39 40 orbi12d 
 |-  ( x = z -> ( ( P e. x \/ x = (/) ) <-> ( P e. z \/ z = (/) ) ) )
42 41 elrab 
 |-  ( z e. { x e. ~P A | ( P e. x \/ x = (/) ) } <-> ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) )
43 38 42 anbi12i 
 |-  ( ( y e. { x e. ~P A | ( P e. x \/ x = (/) ) } /\ z e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) <-> ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) )
44 eleq2 
 |-  ( x = ( y i^i z ) -> ( P e. x <-> P e. ( y i^i z ) ) )
45 eqeq1 
 |-  ( x = ( y i^i z ) -> ( x = (/) <-> ( y i^i z ) = (/) ) )
46 44 45 orbi12d 
 |-  ( x = ( y i^i z ) -> ( ( P e. x \/ x = (/) ) <-> ( P e. ( y i^i z ) \/ ( y i^i z ) = (/) ) ) )
47 inss1 
 |-  ( y i^i z ) C_ y
48 simprll 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> y e. ~P A )
49 48 elpwid 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> y C_ A )
50 47 49 sstrid 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( y i^i z ) C_ A )
51 vex 
 |-  y e. _V
52 51 inex1 
 |-  ( y i^i z ) e. _V
53 52 elpw 
 |-  ( ( y i^i z ) e. ~P A <-> ( y i^i z ) C_ A )
54 50 53 sylibr 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( y i^i z ) e. ~P A )
55 ianor 
 |-  ( -. ( P e. y /\ P e. z ) <-> ( -. P e. y \/ -. P e. z ) )
56 elin 
 |-  ( P e. ( y i^i z ) <-> ( P e. y /\ P e. z ) )
57 55 56 xchnxbir 
 |-  ( -. P e. ( y i^i z ) <-> ( -. P e. y \/ -. P e. z ) )
58 simprlr 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( P e. y \/ y = (/) ) )
59 58 ord 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( -. P e. y -> y = (/) ) )
60 simprrr 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( P e. z \/ z = (/) ) )
61 60 ord 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( -. P e. z -> z = (/) ) )
62 59 61 orim12d 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( ( -. P e. y \/ -. P e. z ) -> ( y = (/) \/ z = (/) ) ) )
63 57 62 biimtrid 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( -. P e. ( y i^i z ) -> ( y = (/) \/ z = (/) ) ) )
64 inss 
 |-  ( ( y C_ (/) \/ z C_ (/) ) -> ( y i^i z ) C_ (/) )
65 ss0b 
 |-  ( y C_ (/) <-> y = (/) )
66 ss0b 
 |-  ( z C_ (/) <-> z = (/) )
67 65 66 orbi12i 
 |-  ( ( y C_ (/) \/ z C_ (/) ) <-> ( y = (/) \/ z = (/) ) )
68 ss0b 
 |-  ( ( y i^i z ) C_ (/) <-> ( y i^i z ) = (/) )
69 64 67 68 3imtr3i 
 |-  ( ( y = (/) \/ z = (/) ) -> ( y i^i z ) = (/) )
70 63 69 syl6 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( -. P e. ( y i^i z ) -> ( y i^i z ) = (/) ) )
71 70 orrd 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( P e. ( y i^i z ) \/ ( y i^i z ) = (/) ) )
72 46 54 71 elrabd 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) ) -> ( y i^i z ) e. { x e. ~P A | ( P e. x \/ x = (/) ) } )
73 72 ex 
 |-  ( ( A e. V /\ P e. A ) -> ( ( ( y e. ~P A /\ ( P e. y \/ y = (/) ) ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) -> ( y i^i z ) e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) )
74 43 73 biimtrid 
 |-  ( ( A e. V /\ P e. A ) -> ( ( y e. { x e. ~P A | ( P e. x \/ x = (/) ) } /\ z e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) -> ( y i^i z ) e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) )
75 74 ralrimivv 
 |-  ( ( A e. V /\ P e. A ) -> A. y e. { x e. ~P A | ( P e. x \/ x = (/) ) } A. z e. { x e. ~P A | ( P e. x \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( P e. x \/ x = (/) ) } )
76 pwexg 
 |-  ( A e. V -> ~P A e. _V )
77 76 adantr 
 |-  ( ( A e. V /\ P e. A ) -> ~P A e. _V )
78 rabexg 
 |-  ( ~P A e. _V -> { x e. ~P A | ( P e. x \/ x = (/) ) } e. _V )
79 istopg 
 |-  ( { x e. ~P A | ( P e. x \/ x = (/) ) } e. _V -> ( { x e. ~P A | ( P e. x \/ x = (/) ) } e. Top <-> ( A. y ( y C_ { x e. ~P A | ( P e. x \/ x = (/) ) } -> U. y e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) /\ A. y e. { x e. ~P A | ( P e. x \/ x = (/) ) } A. z e. { x e. ~P A | ( P e. x \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) ) )
80 77 78 79 3syl 
 |-  ( ( A e. V /\ P e. A ) -> ( { x e. ~P A | ( P e. x \/ x = (/) ) } e. Top <-> ( A. y ( y C_ { x e. ~P A | ( P e. x \/ x = (/) ) } -> U. y e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) /\ A. y e. { x e. ~P A | ( P e. x \/ x = (/) ) } A. z e. { x e. ~P A | ( P e. x \/ x = (/) ) } ( y i^i z ) e. { x e. ~P A | ( P e. x \/ x = (/) ) } ) ) )
81 34 75 80 mpbir2and 
 |-  ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x \/ x = (/) ) } e. Top )
82 eleq2 
 |-  ( x = A -> ( P e. x <-> P e. A ) )
83 eqeq1 
 |-  ( x = A -> ( x = (/) <-> A = (/) ) )
84 82 83 orbi12d 
 |-  ( x = A -> ( ( P e. x \/ x = (/) ) <-> ( P e. A \/ A = (/) ) ) )
85 pwidg 
 |-  ( A e. V -> A e. ~P A )
86 85 adantr 
 |-  ( ( A e. V /\ P e. A ) -> A e. ~P A )
87 animorrl 
 |-  ( ( A e. V /\ P e. A ) -> ( P e. A \/ A = (/) ) )
88 84 86 87 elrabd 
 |-  ( ( A e. V /\ P e. A ) -> A e. { x e. ~P A | ( P e. x \/ x = (/) ) } )
89 elssuni 
 |-  ( A e. { x e. ~P A | ( P e. x \/ x = (/) ) } -> A C_ U. { x e. ~P A | ( P e. x \/ x = (/) ) } )
90 88 89 syl 
 |-  ( ( A e. V /\ P e. A ) -> A C_ U. { x e. ~P A | ( P e. x \/ x = (/) ) } )
91 ssrab2 
 |-  { x e. ~P A | ( P e. x \/ x = (/) ) } C_ ~P A
92 sspwuni 
 |-  ( { x e. ~P A | ( P e. x \/ x = (/) ) } C_ ~P A <-> U. { x e. ~P A | ( P e. x \/ x = (/) ) } C_ A )
93 91 92 mpbi 
 |-  U. { x e. ~P A | ( P e. x \/ x = (/) ) } C_ A
94 93 a1i 
 |-  ( ( A e. V /\ P e. A ) -> U. { x e. ~P A | ( P e. x \/ x = (/) ) } C_ A )
95 90 94 eqssd 
 |-  ( ( A e. V /\ P e. A ) -> A = U. { x e. ~P A | ( P e. x \/ x = (/) ) } )
96 istopon 
 |-  ( { x e. ~P A | ( P e. x \/ x = (/) ) } e. ( TopOn ` A ) <-> ( { x e. ~P A | ( P e. x \/ x = (/) ) } e. Top /\ A = U. { x e. ~P A | ( P e. x \/ x = (/) ) } ) )
97 81 95 96 sylanbrc 
 |-  ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x \/ x = (/) ) } e. ( TopOn ` A ) )