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	|- ( ph -> ( Base ` K ) = ( Base ` L ) )
	tpsprop2d.2	|- ( ph -> ( TopSet ` K ) = ( TopSet ` L ) )
Assertion	tpsprop2d	|- ( ph -> ( K e. TopSp <-> L e. TopSp ) )

Proof

Step	Hyp	Ref	Expression
1		tpsprop2d.1	|- ( ph -> ( Base ` K ) = ( Base ` L ) )
2		tpsprop2d.2	|- ( ph -> ( TopSet ` K ) = ( TopSet ` L ) )
3	1 2	topnpropd	|- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
4	1 3	tpspropd	|- ( ph -> ( K e. TopSp <-> L e. TopSp ) )