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∈V∧P∈A→x∈𝒫A|P∈x∨x=∅=topGen⁡ran⁡x∈A⟼xP

Proof

Step Hyp Ref Expression
1 ppttop ⊢A∈V∧P∈A→y∈𝒫A|P∈y∨y=∅∈TopOn⁡A
2 topontop ⊢y∈𝒫A|P∈y∨y=∅∈TopOn⁡A→y∈𝒫A|P∈y∨y=∅∈Top
3 1 2 syl ⊢A∈V∧P∈A→y∈𝒫A|P∈y∨y=∅∈Top
4 eleq2 ⊢y=xP→P∈y↔P∈xP
5 eqeq1 ⊢y=xP→y=∅↔xP=∅
6 4 5 orbi12d ⊢y=xP→P∈y∨y=∅↔P∈xP∨xP=∅
7 simpr ⊢A∈V∧P∈A∧x∈A→x∈A
8 simplr ⊢A∈V∧P∈A∧x∈A→P∈A
9 7 8 prssd ⊢A∈V∧P∈A∧x∈A→xP⊆A
10 prex ⊢xP∈V
11 10 elpw ⊢xP∈𝒫A↔xP⊆A
12 9 11 sylibr ⊢A∈V∧P∈A∧x∈A→xP∈𝒫A
13 prid2g ⊢P∈A→P∈xP
14 13 ad2antlr ⊢A∈V∧P∈A∧x∈A→P∈xP
15 14 orcd ⊢A∈V∧P∈A∧x∈A→P∈xP∨xP=∅
16 6 12 15 elrabd ⊢A∈V∧P∈A∧x∈A→xP∈y∈𝒫A|P∈y∨y=∅
17 16 fmpttd ⊢A∈V∧P∈A→x∈A⟼xP:A⟶y∈𝒫A|P∈y∨y=∅
18 17 frnd ⊢A∈V∧P∈A→ran⁡x∈A⟼xP⊆y∈𝒫A|P∈y∨y=∅
19 eleq2 ⊢y=z→P∈y↔P∈z
20 eqeq1 ⊢y=z→y=∅↔z=∅
21 19 20 orbi12d ⊢y=z→P∈y∨y=∅↔P∈z∨z=∅
22 21 elrab ⊢z∈y∈𝒫A|P∈y∨y=∅↔z∈𝒫A∧P∈z∨z=∅
23 elpwi ⊢z∈𝒫A→z⊆A
24 23 ad2antrl ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅→z⊆A
25 24 sselda ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅∧w∈z→w∈A
26 prid1g ⊢w∈z→w∈wP
27 26 adantl ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅∧w∈z→w∈wP
28 simpr ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅∧w∈z→w∈z
29 n0i ⊢w∈z→¬z=∅
30 29 adantl ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅∧w∈z→¬z=∅
31 simplrr ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅∧w∈z→P∈z∨z=∅
32 31 ord ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅∧w∈z→¬P∈z→z=∅
33 30 32 mt3d ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅∧w∈z→P∈z
34 28 33 prssd ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅∧w∈z→wP⊆z
35 preq1 ⊢x=w→xP=wP
36 35 eleq2d ⊢x=w→w∈xP↔w∈wP
37 35 sseq1d ⊢x=w→xP⊆z↔wP⊆z
38 36 37 anbi12d ⊢x=w→w∈xP∧xP⊆z↔w∈wP∧wP⊆z
39 38 rspcev ⊢w∈A∧w∈wP∧wP⊆z→∃x∈Aw∈xP∧xP⊆z
40 25 27 34 39 syl12anc ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅∧w∈z→∃x∈Aw∈xP∧xP⊆z
41 10 rgenw ⊢∀x∈AxP∈V
42 eqid ⊢x∈A⟼xP=x∈A⟼xP
43 eleq2 ⊢v=xP→w∈v↔w∈xP
44 sseq1 ⊢v=xP→v⊆z↔xP⊆z
45 43 44 anbi12d ⊢v=xP→w∈v∧v⊆z↔w∈xP∧xP⊆z
46 42 45 rexrnmptw ⊢∀x∈AxP∈V→∃v∈ran⁡x∈A⟼xPw∈v∧v⊆z↔∃x∈Aw∈xP∧xP⊆z
47 41 46 ax-mp ⊢∃v∈ran⁡x∈A⟼xPw∈v∧v⊆z↔∃x∈Aw∈xP∧xP⊆z
48 40 47 sylibr ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅∧w∈z→∃v∈ran⁡x∈A⟼xPw∈v∧v⊆z
49 48 ralrimiva ⊢A∈V∧P∈A∧z∈𝒫A∧P∈z∨z=∅→∀w∈z∃v∈ran⁡x∈A⟼xPw∈v∧v⊆z
50 49 ex ⊢A∈V∧P∈A→z∈𝒫A∧P∈z∨z=∅→∀w∈z∃v∈ran⁡x∈A⟼xPw∈v∧v⊆z
51 22 50 biimtrid ⊢A∈V∧P∈A→z∈y∈𝒫A|P∈y∨y=∅→∀w∈z∃v∈ran⁡x∈A⟼xPw∈v∧v⊆z
52 51 ralrimiv ⊢A∈V∧P∈A→∀z∈y∈𝒫A|P∈y∨y=∅∀w∈z∃v∈ran⁡x∈A⟼xPw∈v∧v⊆z
53 basgen2 ⊢y∈𝒫A|P∈y∨y=∅∈Top∧ran⁡x∈A⟼xP⊆y∈𝒫A|P∈y∨y=∅∧∀z∈y∈𝒫A|P∈y∨y=∅∀w∈z∃v∈ran⁡x∈A⟼xPw∈v∧v⊆z→topGen⁡ran⁡x∈A⟼xP=y∈𝒫A|P∈y∨y=∅
54 3 18 52 53 syl3anc ⊢A∈V∧P∈A→topGen⁡ran⁡x∈A⟼xP=y∈𝒫A|P∈y∨y=∅
55 eleq2 ⊢y=x→P∈y↔P∈x
56 eqeq1 ⊢y=x→y=∅↔x=∅
57 55 56 orbi12d ⊢y=x→P∈y∨y=∅↔P∈x∨x=∅
58 57 cbvrabv ⊢y∈𝒫A|P∈y∨y=∅=x∈𝒫A|P∈x∨x=∅
59 54 58 eqtr2di ⊢A∈V∧P∈A→x∈𝒫A|P∈x∨x=∅=topGen⁡ran⁡x∈A⟼xP