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

Metamath Proof Explorer

Theorem regtop

Description: A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion regtop ⊢ J ∈ Reg → J ∈ Top

Proof

Step Hyp Ref Expression
1 isreg ⊢ J ∈ Reg ↔ J ∈ Top ∧ ∀ x ∈ J ∀ y ∈ x ∃ z ∈ J y ∈ z ∧ cls ⁡ J ⁡ z ⊆ x
2 1 simplbi ⊢ J ∈ Reg → J ∈ Top