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 syl5bi
 |-  ( ( ( 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 syl5bi
 |-  ( ( ( 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 syl5bi
 |-  ( ( 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 syl5bi
 |-  ( ( ( 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 syl5bi
 |-  ( ( 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 ) )