Metamath Proof Explorer


Theorem istpsi

Description: Properties that determine a topological space. (Contributed by NM, 20-Oct-2012)

Ref Expression
Hypotheses istpsi.b ( Base ‘ 𝐾 ) = 𝐴
istpsi.j ( TopOpen ‘ 𝐾 ) = 𝐽
istpsi.1 𝐴 = 𝐽
istpsi.2 𝐽 ∈ Top
Assertion istpsi 𝐾 ∈ TopSp

Proof

Step Hyp Ref Expression
1 istpsi.b ( Base ‘ 𝐾 ) = 𝐴
2 istpsi.j ( TopOpen ‘ 𝐾 ) = 𝐽
3 istpsi.1 𝐴 = 𝐽
4 istpsi.2 𝐽 ∈ Top
5 1 eqcomi 𝐴 = ( Base ‘ 𝐾 )
6 2 eqcomi 𝐽 = ( TopOpen ‘ 𝐾 )
7 5 6 istps2 ( 𝐾 ∈ TopSp ↔ ( 𝐽 ∈ Top ∧ 𝐴 = 𝐽 ) )
8 4 3 7 mpbir2an 𝐾 ∈ TopSp