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 φ Base K = Base L
tpsprop2d.2 φ TopSet K = TopSet L
Assertion tpsprop2d φ K TopSp L TopSp

Proof

Step Hyp Ref Expression
1 tpsprop2d.1 φ Base K = Base L
2 tpsprop2d.2 φ TopSet K = TopSet L
3 1 2 topnpropd φ TopOpen K = TopOpen L
4 1 3 tpspropd φ K TopSp L TopSp