Metamath Proof Explorer

Theorem tpspropd

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

		Ref	Expression
	Hypotheses	tpspropd.1	$⊢ φ \to {Base}_{K} = {Base}_{L}$
		tpspropd.2	$⊢ φ \to TopOpen (K) = TopOpen (L)$
	Assertion	tpspropd	$⊢ φ \to (K \in TopSp \leftrightarrow L \in TopSp)$

Proof

Step	Hyp	Ref	Expression
1		tpspropd.1	$⊢ φ \to {Base}_{K} = {Base}_{L}$
2		tpspropd.2	$⊢ φ \to TopOpen (K) = TopOpen (L)$
3	1	fveq2d	$⊢ φ \to TopOn ({Base}_{K}) = TopOn ({Base}_{L})$
4	2 3	eleq12d	$⊢ φ \to (TopOpen (K) \in TopOn ({Base}_{K}) \leftrightarrow TopOpen (L) \in TopOn ({Base}_{L}))$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		eqid	$⊢ TopOpen (K) = TopOpen (K)$
7	5 6	istps	$⊢ K \in TopSp \leftrightarrow TopOpen (K) \in TopOn ({Base}_{K})$
8		eqid	$⊢ {Base}_{L} = {Base}_{L}$
9		eqid	$⊢ TopOpen (L) = TopOpen (L)$
10	8 9	istps	$⊢ L \in TopSp \leftrightarrow TopOpen (L) \in TopOn ({Base}_{L})$
11	4 7 10	3bitr4g	$⊢ φ \to (K \in TopSp \leftrightarrow L \in TopSp)$