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

Metamath Proof Explorer

Theorem istps2

Description: Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012)

Ref Expression
Hypotheses istps.a ⊢ A = Base K
istps.j ⊢ J = TopOpen ⁡ K
Assertion istps2 ⊢ K ∈ TopSp ↔ J ∈ Top ∧ A = ⋃ J

Proof

Step Hyp Ref Expression
1 istps.a ⊢ A = Base K
2 istps.j ⊢ J = TopOpen ⁡ K
3 1 2 istps ⊢ K ∈ TopSp ↔ J ∈ TopOn ⁡ A
4 istopon ⊢ J ∈ TopOn ⁡ A ↔ J ∈ Top ∧ A = ⋃ J
5 3 4 bitri ⊢ K ∈ TopSp ↔ J ∈ Top ∧ A = ⋃ J