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ω )