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

Metamath Proof Explorer

Theorem tpsuni

Description: The base set of a topological space. (Contributed by FL, 27-Jun-2014)

Ref Expression
Hypotheses istps.a ⊢ A = Base K
istps.j ⊢ J = TopOpen ⁡ K
Assertion tpsuni ⊢ K ∈ TopSp → A = ⋃ J

Proof

Step Hyp Ref Expression
1 istps.a ⊢ A = Base K
2 istps.j ⊢ J = TopOpen ⁡ K
3 1 2 istps2 ⊢ K ∈ TopSp ↔ J ∈ Top ∧ A = ⋃ J
4 3 simprbi ⊢ K ∈ TopSp → A = ⋃ J