# 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 syl5bi ( ( 𝐴𝑉𝑃𝐴 ) → ( 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑦𝑦 = ∅ ) } → ∀ 𝑤𝑧𝑣 ∈ 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 ( 𝑥𝐴 ↦ { 𝑥 , 𝑃 } ) ) )