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

Metamath Proof Explorer

Theorem dis1stc

Description: A discrete space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion dis1stc ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ 1stω )

Proof

Step Hyp Ref Expression
1 vsnex ⊢ { 𝑥 } ∈ V
2 distop ⊢ ( { 𝑥 } ∈ V → 𝒫 { 𝑥 } ∈ Top )
3 1 2 ax-mp ⊢ 𝒫 { 𝑥 } ∈ Top
4 tgtop ⊢ ( 𝒫 { 𝑥 } ∈ Top → ( topGen ‘ 𝒫 { 𝑥 } ) = 𝒫 { 𝑥 } )
5 3 4 ax-mp ⊢ ( topGen ‘ 𝒫 { 𝑥 } ) = 𝒫 { 𝑥 }
6 topbas ⊢ ( 𝒫 { 𝑥 } ∈ Top → 𝒫 { 𝑥 } ∈ TopBases )
7 3 6 ax-mp ⊢ 𝒫 { 𝑥 } ∈ TopBases
8 snfi ⊢ { 𝑥 } ∈ Fin
9 pwfi ⊢ ( { 𝑥 } ∈ Fin ↔ 𝒫 { 𝑥 } ∈ Fin )
10 8 9 mpbi ⊢ 𝒫 { 𝑥 } ∈ Fin
11 isfinite ⊢ ( 𝒫 { 𝑥 } ∈ Fin ↔ 𝒫 { 𝑥 } ≺ ω )
12 10 11 mpbi ⊢ 𝒫 { 𝑥 } ≺ ω
13 sdomdom ⊢ ( 𝒫 { 𝑥 } ≺ ω → 𝒫 { 𝑥 } ≼ ω )
14 12 13 ax-mp ⊢ 𝒫 { 𝑥 } ≼ ω
15 2ndci ⊢ ( ( 𝒫 { 𝑥 } ∈ TopBases ∧ 𝒫 { 𝑥 } ≼ ω ) → ( topGen ‘ 𝒫 { 𝑥 } ) ∈ 2ndω )
16 7 14 15 mp2an ⊢ ( topGen ‘ 𝒫 { 𝑥 } ) ∈ 2ndω
17 5 16 eqeltrri ⊢ 𝒫 { 𝑥 } ∈ 2ndω
18 2ndc1stc ⊢ ( 𝒫 { 𝑥 } ∈ 2ndω → 𝒫 { 𝑥 } ∈ 1stω )
19 17 18 ax-mp ⊢ 𝒫 { 𝑥 } ∈ 1stω
20 19 rgenw ⊢ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 1stω
21 dislly ⊢ ( 𝑋 ∈ 𝑉 → ( 𝒫 𝑋 ∈ Locally 1stω ↔ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 1stω ) )
22 20 21 mpbiri ⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Locally 1stω )
23 lly1stc ⊢ Locally 1stω = 1stω
24 22 23 eleqtrdi ⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ 1stω )