Theorem istps2

Description: Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012)

	Ref	Expression
Hypotheses	istps.a	⊢ 𝐴 = ( Base ‘ 𝐾 )
	istps.j	⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
Assertion	istps2	⊢ ( 𝐾 ∈ TopSp ↔ ( 𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		istps.a	⊢ 𝐴 = ( Base ‘ 𝐾 )
2		istps.j	⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
3	1 2	istps	⊢ ( 𝐾 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐴 ) )
4		istopon	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) ↔ ( 𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽 ) )
5	3 4	bitri	⊢ ( 𝐾 ∈ TopSp ↔ ( 𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽 ) )