This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑥 ∨ 𝑥 = ∅ ) } = ( topGen ‘ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 , 𝑃 } ) ) )

Proof

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