Metamath Proof Explorer


Theorem tpsuni

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

Ref Expression
Hypotheses istps.a 𝐴 = ( Base ‘ 𝐾 )
istps.j 𝐽 = ( TopOpen ‘ 𝐾 )
Assertion tpsuni ( 𝐾 ∈ TopSp → 𝐴 = 𝐽 )

Proof

Step Hyp Ref Expression
1 istps.a 𝐴 = ( Base ‘ 𝐾 )
2 istps.j 𝐽 = ( TopOpen ‘ 𝐾 )
3 1 2 istps2 ( 𝐾 ∈ TopSp ↔ ( 𝐽 ∈ Top ∧ 𝐴 = 𝐽 ) )
4 3 simprbi ( 𝐾 ∈ TopSp → 𝐴 = 𝐽 )