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

Metamath Proof Explorer

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	$⊢ φ \to {Base}_{K} = {Base}_{L}$
	tpsprop2d.2	$⊢ φ \to TopSet (K) = TopSet (L)$
Assertion	tpsprop2d	$⊢ φ \to (K \in TopSp \leftrightarrow L \in TopSp)$

Step	Hyp	Ref	Expression
1		tpsprop2d.1	$⊢ φ \to {Base}_{K} = {Base}_{L}$
2		tpsprop2d.2	$⊢ φ \to TopSet (K) = TopSet (L)$
3	1 2	topnpropd	$⊢ φ \to TopOpen (K) = TopOpen (L)$
4	1 3	tpspropd	$⊢ φ \to (K \in TopSp \leftrightarrow L \in TopSp)$