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

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	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
		tpspropd.2	⊢ ( 𝜑 → ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐿 ) )
	Assertion	tpspropd	⊢ ( 𝜑 → ( 𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp ) )

Proof

Step	Hyp	Ref	Expression
1		tpspropd.1	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
2		tpspropd.2	⊢ ( 𝜑 → ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐿 ) )
3	1	fveq2d	⊢ ( 𝜑 → ( TopOn ‘ ( Base ‘ 𝐾 ) ) = ( TopOn ‘ ( Base ‘ 𝐿 ) ) )
4	2 3	eleq12d	⊢ ( 𝜑 → ( ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) ↔ ( TopOpen ‘ 𝐿 ) ∈ ( TopOn ‘ ( Base ‘ 𝐿 ) ) ) )
5		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6		eqid	⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 )
7	5 6	istps	⊢ ( 𝐾 ∈ TopSp ↔ ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) )
8		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
9		eqid	⊢ ( TopOpen ‘ 𝐿 ) = ( TopOpen ‘ 𝐿 )
10	8 9	istps	⊢ ( 𝐿 ∈ TopSp ↔ ( TopOpen ‘ 𝐿 ) ∈ ( TopOn ‘ ( Base ‘ 𝐿 ) ) )
11	4 7 10	3bitr4g	⊢ ( 𝜑 → ( 𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp ) )