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	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
	tpsprop2d.2	$$⊢\phi \to \mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(L\right)$$
Assertion	tpsprop2d	$$⊢\phi \to \left(K\in \mathrm{TopSp}\leftrightarrow L\in \mathrm{TopSp}\right)$$

Proof

Step	Hyp	Ref	Expression
1		tpsprop2d.1	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
2		tpsprop2d.2	$$⊢\phi \to \mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(L\right)$$
3	1 2	topnpropd	$$⊢\phi \to \mathrm{TopOpen}\left(K\right)=\mathrm{TopOpen}\left(L\right)$$
4	1 3	tpspropd	$$⊢\phi \to \left(K\in \mathrm{TopSp}\leftrightarrow L\in \mathrm{TopSp}\right)$$