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