Metamath Proof Explorer

Theorem pptbas

Description: The particular point topology is generated by a basis consisting of pairs { x , P } for each x e. A . (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion pptbas 
|- ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x \/ x = (/) ) } = ( topGen ` ran ( x e. A |-> { x , P } ) ) )

Proof

Step Hyp Ref Expression
1 ppttop 
 |-  ( ( A e. V /\ P e. A ) -> { y e. ~P A | ( P e. y \/ y = (/) ) } e. ( TopOn ` A ) )
2 topontop 
 |-  ( { y e. ~P A | ( P e. y \/ y = (/) ) } e. ( TopOn ` A ) -> { y e. ~P A | ( P e. y \/ y = (/) ) } e. Top )
3 1 2 syl 
 |-  ( ( A e. V /\ P e. A ) -> { y e. ~P A | ( P e. y \/ y = (/) ) } e. Top )
4 eleq2 
 |-  ( y = { x , P } -> ( P e. y <-> P e. { x , P } ) )
5 eqeq1 
 |-  ( y = { x , P } -> ( y = (/) <-> { x , P } = (/) ) )
6 4 5 orbi12d 
 |-  ( y = { x , P } -> ( ( P e. y \/ y = (/) ) <-> ( P e. { x , P } \/ { x , P } = (/) ) ) )
7 simpr 
 |-  ( ( ( A e. V /\ P e. A ) /\ x e. A ) -> x e. A )
8 simplr 
 |-  ( ( ( A e. V /\ P e. A ) /\ x e. A ) -> P e. A )
9 7 8 prssd 
 |-  ( ( ( A e. V /\ P e. A ) /\ x e. A ) -> { x , P } C_ A )
10 prex 
 |-  { x , P } e. _V
11 10 elpw 
 |-  ( { x , P } e. ~P A <-> { x , P } C_ A )
12 9 11 sylibr 
 |-  ( ( ( A e. V /\ P e. A ) /\ x e. A ) -> { x , P } e. ~P A )
13 prid2g 
 |-  ( P e. A -> P e. { x , P } )
14 13 ad2antlr 
 |-  ( ( ( A e. V /\ P e. A ) /\ x e. A ) -> P e. { x , P } )
15 14 orcd 
 |-  ( ( ( A e. V /\ P e. A ) /\ x e. A ) -> ( P e. { x , P } \/ { x , P } = (/) ) )
16 6 12 15 elrabd 
 |-  ( ( ( A e. V /\ P e. A ) /\ x e. A ) -> { x , P } e. { y e. ~P A | ( P e. y \/ y = (/) ) } )
17 16 fmpttd 
 |-  ( ( A e. V /\ P e. A ) -> ( x e. A |-> { x , P } ) : A --> { y e. ~P A | ( P e. y \/ y = (/) ) } )
18 17 frnd 
 |-  ( ( A e. V /\ P e. A ) -> ran ( x e. A |-> { x , P } ) C_ { y e. ~P A | ( P e. y \/ y = (/) ) } )
19 eleq2 
 |-  ( y = z -> ( P e. y <-> P e. z ) )
20 eqeq1 
 |-  ( y = z -> ( y = (/) <-> z = (/) ) )
21 19 20 orbi12d 
 |-  ( y = z -> ( ( P e. y \/ y = (/) ) <-> ( P e. z \/ z = (/) ) ) )
22 21 elrab 
 |-  ( z e. { y e. ~P A | ( P e. y \/ y = (/) ) } <-> ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) )
23 elpwi 
 |-  ( z e. ~P A -> z C_ A )
24 23 ad2antrl 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) -> z C_ A )
25 24 sselda 
 |-  ( ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) /\ w e. z ) -> w e. A )
26 prid1g 
 |-  ( w e. z -> w e. { w , P } )
27 26 adantl 
 |-  ( ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) /\ w e. z ) -> w e. { w , P } )
28 simpr 
 |-  ( ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) /\ w e. z ) -> w e. z )
29 n0i 
 |-  ( w e. z -> -. z = (/) )
30 29 adantl 
 |-  ( ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) /\ w e. z ) -> -. z = (/) )
31 simplrr 
 |-  ( ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) /\ w e. z ) -> ( P e. z \/ z = (/) ) )
32 31 ord 
 |-  ( ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) /\ w e. z ) -> ( -. P e. z -> z = (/) ) )
33 30 32 mt3d 
 |-  ( ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) /\ w e. z ) -> P e. z )
34 28 33 prssd 
 |-  ( ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) /\ w e. z ) -> { w , P } C_ z )
35 preq1 
 |-  ( x = w -> { x , P } = { w , P } )
36 35 eleq2d 
 |-  ( x = w -> ( w e. { x , P } <-> w e. { w , P } ) )
37 35 sseq1d 
 |-  ( x = w -> ( { x , P } C_ z <-> { w , P } C_ z ) )
38 36 37 anbi12d 
 |-  ( x = w -> ( ( w e. { x , P } /\ { x , P } C_ z ) <-> ( w e. { w , P } /\ { w , P } C_ z ) ) )
39 38 rspcev 
 |-  ( ( w e. A /\ ( w e. { w , P } /\ { w , P } C_ z ) ) -> E. x e. A ( w e. { x , P } /\ { x , P } C_ z ) )
40 25 27 34 39 syl12anc 
 |-  ( ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) /\ w e. z ) -> E. x e. A ( w e. { x , P } /\ { x , P } C_ z ) )
41 10 rgenw 
 |-  A. x e. A { x , P } e. _V
42 eqid 
 |-  ( x e. A |-> { x , P } ) = ( x e. A |-> { x , P } )
43 eleq2 
 |-  ( v = { x , P } -> ( w e. v <-> w e. { x , P } ) )
44 sseq1 
 |-  ( v = { x , P } -> ( v C_ z <-> { x , P } C_ z ) )
45 43 44 anbi12d 
 |-  ( v = { x , P } -> ( ( w e. v /\ v C_ z ) <-> ( w e. { x , P } /\ { x , P } C_ z ) ) )
46 42 45 rexrnmptw 
 |-  ( A. x e. A { x , P } e. _V -> ( E. v e. ran ( x e. A |-> { x , P } ) ( w e. v /\ v C_ z ) <-> E. x e. A ( w e. { x , P } /\ { x , P } C_ z ) ) )
47 41 46 ax-mp 
 |-  ( E. v e. ran ( x e. A |-> { x , P } ) ( w e. v /\ v C_ z ) <-> E. x e. A ( w e. { x , P } /\ { x , P } C_ z ) )
48 40 47 sylibr 
 |-  ( ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) /\ w e. z ) -> E. v e. ran ( x e. A |-> { x , P } ) ( w e. v /\ v C_ z ) )
49 48 ralrimiva 
 |-  ( ( ( A e. V /\ P e. A ) /\ ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) ) -> A. w e. z E. v e. ran ( x e. A |-> { x , P } ) ( w e. v /\ v C_ z ) )
50 49 ex 
 |-  ( ( A e. V /\ P e. A ) -> ( ( z e. ~P A /\ ( P e. z \/ z = (/) ) ) -> A. w e. z E. v e. ran ( x e. A |-> { x , P } ) ( w e. v /\ v C_ z ) ) )
51 22 50 syl5bi 
 |-  ( ( A e. V /\ P e. A ) -> ( z e. { y e. ~P A | ( P e. y \/ y = (/) ) } -> A. w e. z E. v e. ran ( x e. A |-> { x , P } ) ( w e. v /\ v C_ z ) ) )
52 51 ralrimiv 
 |-  ( ( A e. V /\ P e. A ) -> A. z e. { y e. ~P A | ( P e. y \/ y = (/) ) } A. w e. z E. v e. ran ( x e. A |-> { x , P } ) ( w e. v /\ v C_ z ) )
53 basgen2 
 |-  ( ( { y e. ~P A | ( P e. y \/ y = (/) ) } e. Top /\ ran ( x e. A |-> { x , P } ) C_ { y e. ~P A | ( P e. y \/ y = (/) ) } /\ A. z e. { y e. ~P A | ( P e. y \/ y = (/) ) } A. w e. z E. v e. ran ( x e. A |-> { x , P } ) ( w e. v /\ v C_ z ) ) -> ( topGen ` ran ( x e. A |-> { x , P } ) ) = { y e. ~P A | ( P e. y \/ y = (/) ) } )
54 3 18 52 53 syl3anc 
 |-  ( ( A e. V /\ P e. A ) -> ( topGen ` ran ( x e. A |-> { x , P } ) ) = { y e. ~P A | ( P e. y \/ y = (/) ) } )
55 eleq2 
 |-  ( y = x -> ( P e. y <-> P e. x ) )
56 eqeq1 
 |-  ( y = x -> ( y = (/) <-> x = (/) ) )
57 55 56 orbi12d 
 |-  ( y = x -> ( ( P e. y \/ y = (/) ) <-> ( P e. x \/ x = (/) ) ) )
58 57 cbvrabv 
 |-  { y e. ~P A | ( P e. y \/ y = (/) ) } = { x e. ~P A | ( P e. x \/ x = (/) ) }
59 54 58 eqtr2di 
 |-  ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x \/ x = (/) ) } = ( topGen ` ran ( x e. A |-> { x , P } ) ) )