Theorem 1stctop

Description: A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009)

	Ref	Expression
Assertion	1stctop	⊢ ( 𝐽 ∈ 1stω → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	is1stc	⊢ ( 𝐽 ∈ 1stω ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∃ 𝑦 ∈ 𝒫 𝐽 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ ( 𝑦 ∩ 𝒫 𝑧 ) ) ) ) )
3	2	simplbi	⊢ ( 𝐽 ∈ 1stω → 𝐽 ∈ Top )