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

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