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 snex { 𝑥 } ∈ 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ω )