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

Metamath Proof Explorer

Theorem 1stctop

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

Ref Expression
Assertion 1stctop ⊢ J ∈ 1 st 𝜔 → J ∈ Top

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 is1stc ⊢ J ∈ 1 st 𝜔 ↔ J ∈ Top ∧ ∀ x ∈ ⋃ J ∃ y ∈ 𝒫 J y ≼ ω ∧ ∀ z ∈ J x ∈ z → x ∈ ⋃ y ∩ 𝒫 z
3 2 simplbi ⊢ J ∈ 1 st 𝜔 → J ∈ Top