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 ) )