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 φBaseK=BaseL
tpsprop2d.2 φTopSetK=TopSetL
Assertion tpsprop2d φKTopSpLTopSp

Proof

Step Hyp Ref Expression
1 tpsprop2d.1 φBaseK=BaseL
2 tpsprop2d.2 φTopSetK=TopSetL
3 1 2 topnpropd φTopOpenK=TopOpenL
4 1 3 tpspropd φKTopSpLTopSp