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 ⟼ x P

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 = x P → P ∈ y ↔ P ∈ x P
5 eqeq1 ⊢ y = x P → y = ∅ ↔ x P = ∅
6 4 5 orbi12d ⊢ y = x P → P ∈ y ∨ y = ∅ ↔ P ∈ x P ∨ x P = ∅
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 → x P ⊆ A
10 prex ⊢ x P ∈ V
11 10 elpw ⊢ x P ∈ 𝒫 A ↔ x P ⊆ A
12 9 11 sylibr ⊢ A ∈ V ∧ P ∈ A ∧ x ∈ A → x P ∈ 𝒫 A
13 prid2g ⊢ P ∈ A → P ∈ x P
14 13 ad2antlr ⊢ A ∈ V ∧ P ∈ A ∧ x ∈ A → P ∈ x P
15 14 orcd ⊢ A ∈ V ∧ P ∈ A ∧ x ∈ A → P ∈ x P ∨ x P = ∅
16 6 12 15 elrabd ⊢ A ∈ V ∧ P ∈ A ∧ x ∈ A → x P ∈ y ∈ 𝒫 A | P ∈ y ∨ y = ∅
17 16 fmpttd ⊢ A ∈ V ∧ P ∈ A → x ∈ A ⟼ x P : A ⟶ y ∈ 𝒫 A | P ∈ y ∨ y = ∅
18 17 frnd ⊢ A ∈ V ∧ P ∈ A → ran ⁡ x ∈ A ⟼ x P ⊆ 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 ∈ w P
27 26 adantl ⊢ A ∈ V ∧ P ∈ A ∧ z ∈ 𝒫 A ∧ P ∈ z ∨ z = ∅ ∧ w ∈ z → w ∈ w P
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 → w P ⊆ z
35 preq1 ⊢ x = w → x P = w P
36 35 eleq2d ⊢ x = w → w ∈ x P ↔ w ∈ w P
37 35 sseq1d ⊢ x = w → x P ⊆ z ↔ w P ⊆ z
38 36 37 anbi12d ⊢ x = w → w ∈ x P ∧ x P ⊆ z ↔ w ∈ w P ∧ w P ⊆ z
39 38 rspcev ⊢ w ∈ A ∧ w ∈ w P ∧ w P ⊆ z → ∃ x ∈ A w ∈ x P ∧ x P ⊆ z
40 25 27 34 39 syl12anc ⊢ A ∈ V ∧ P ∈ A ∧ z ∈ 𝒫 A ∧ P ∈ z ∨ z = ∅ ∧ w ∈ z → ∃ x ∈ A w ∈ x P ∧ x P ⊆ z
41 10 rgenw ⊢ ∀ x ∈ A x P ∈ V
42 eqid ⊢ x ∈ A ⟼ x P = x ∈ A ⟼ x P
43 eleq2 ⊢ v = x P → w ∈ v ↔ w ∈ x P
44 sseq1 ⊢ v = x P → v ⊆ z ↔ x P ⊆ z
45 43 44 anbi12d ⊢ v = x P → w ∈ v ∧ v ⊆ z ↔ w ∈ x P ∧ x P ⊆ z
46 42 45 rexrnmptw ⊢ ∀ x ∈ A x P ∈ V → ∃ v ∈ ran ⁡ x ∈ A ⟼ x P w ∈ v ∧ v ⊆ z ↔ ∃ x ∈ A w ∈ x P ∧ x P ⊆ z
47 41 46 ax-mp ⊢ ∃ v ∈ ran ⁡ x ∈ A ⟼ x P w ∈ v ∧ v ⊆ z ↔ ∃ x ∈ A w ∈ x P ∧ x P ⊆ z
48 40 47 sylibr ⊢ A ∈ V ∧ P ∈ A ∧ z ∈ 𝒫 A ∧ P ∈ z ∨ z = ∅ ∧ w ∈ z → ∃ v ∈ ran ⁡ x ∈ A ⟼ x P w ∈ v ∧ v ⊆ z
49 48 ralrimiva ⊢ A ∈ V ∧ P ∈ A ∧ z ∈ 𝒫 A ∧ P ∈ z ∨ z = ∅ → ∀ w ∈ z ∃ v ∈ ran ⁡ x ∈ A ⟼ x P w ∈ v ∧ v ⊆ z
50 49 ex ⊢ A ∈ V ∧ P ∈ A → z ∈ 𝒫 A ∧ P ∈ z ∨ z = ∅ → ∀ w ∈ z ∃ v ∈ ran ⁡ x ∈ A ⟼ x P w ∈ v ∧ v ⊆ z
51 22 50 syl5bi ⊢ A ∈ V ∧ P ∈ A → z ∈ y ∈ 𝒫 A | P ∈ y ∨ y = ∅ → ∀ w ∈ z ∃ v ∈ ran ⁡ x ∈ A ⟼ x P w ∈ v ∧ v ⊆ z
52 51 ralrimiv ⊢ A ∈ V ∧ P ∈ A → ∀ z ∈ y ∈ 𝒫 A | P ∈ y ∨ y = ∅ ∀ w ∈ z ∃ v ∈ ran ⁡ x ∈ A ⟼ x P w ∈ v ∧ v ⊆ z
53 basgen2 ⊢ y ∈ 𝒫 A | P ∈ y ∨ y = ∅ ∈ Top ∧ ran ⁡ x ∈ A ⟼ x P ⊆ y ∈ 𝒫 A | P ∈ y ∨ y = ∅ ∧ ∀ z ∈ y ∈ 𝒫 A | P ∈ y ∨ y = ∅ ∀ w ∈ z ∃ v ∈ ran ⁡ x ∈ A ⟼ x P w ∈ v ∧ v ⊆ z → topGen ⁡ ran ⁡ x ∈ A ⟼ x P = y ∈ 𝒫 A | P ∈ y ∨ y = ∅
54 3 18 52 53 syl3anc ⊢ A ∈ V ∧ P ∈ A → topGen ⁡ ran ⁡ x ∈ A ⟼ x P = 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 ⟼ x P