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

Proof

Step Hyp Ref Expression
1 tpspropd.1 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
2 tpspropd.2 
 |-  ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
3 1 fveq2d 
 |-  ( ph -> ( TopOn ` ( Base ` K ) ) = ( TopOn ` ( Base ` L ) ) )
4 2 3 eleq12d 
 |-  ( ph -> ( ( TopOpen ` K ) e. ( TopOn ` ( Base ` K ) ) <-> ( TopOpen ` L ) e. ( TopOn ` ( Base ` L ) ) ) )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( TopOpen ` K ) = ( TopOpen ` K )
7 5 6 istps 
 |-  ( K e. TopSp <-> ( TopOpen ` K ) e. ( TopOn ` ( Base ` K ) ) )
8 eqid 
 |-  ( Base ` L ) = ( Base ` L )
9 eqid 
 |-  ( TopOpen ` L ) = ( TopOpen ` L )
10 8 9 istps 
 |-  ( L e. TopSp <-> ( TopOpen ` L ) e. ( TopOn ` ( Base ` L ) ) )
11 4 7 10 3bitr4g 
 |-  ( ph -> ( K e. TopSp <-> L e. TopSp ) )