Theorem tpsprop2d

Description: A topological space depends only on the base and topology components. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypotheses	tpsprop2d.1	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
	tpsprop2d.2	⊢ ( 𝜑 → ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐿 ) )
Assertion	tpsprop2d	⊢ ( 𝜑 → ( 𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp ) )

Proof

Step	Hyp	Ref	Expression
1		tpsprop2d.1	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
2		tpsprop2d.2	⊢ ( 𝜑 → ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐿 ) )
3	1 2	topnpropd	⊢ ( 𝜑 → ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐿 ) )
4	1 3	tpspropd	⊢ ( 𝜑 → ( 𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp ) )