Metamath Proof Explorer

Theorem topnpropd

Description: The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006)

Ref Expression
Hypotheses topnpropd.1 
|- ( ph -> ( Base ` K ) = ( Base ` L ) )
topnpropd.2 
|- ( ph -> ( TopSet ` K ) = ( TopSet ` L ) )
Assertion topnpropd 
|- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )

Proof

Step Hyp Ref Expression
1 topnpropd.1 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
2 topnpropd.2 
 |-  ( ph -> ( TopSet ` K ) = ( TopSet ` L ) )
3 2 1 oveq12d 
 |-  ( ph -> ( ( TopSet ` K ) |`t ( Base ` K ) ) = ( ( TopSet ` L ) |`t ( Base ` L ) ) )
4 eqid 
 |-  ( Base ` K ) = ( Base ` K )
5 eqid 
 |-  ( TopSet ` K ) = ( TopSet ` K )
6 4 5 topnval 
 |-  ( ( TopSet ` K ) |`t ( Base ` K ) ) = ( TopOpen ` K )
7 eqid 
 |-  ( Base ` L ) = ( Base ` L )
8 eqid 
 |-  ( TopSet ` L ) = ( TopSet ` L )
9 7 8 topnval 
 |-  ( ( TopSet ` L ) |`t ( Base ` L ) ) = ( TopOpen ` L )
10 3 6 9 3eqtr3g 
 |-  ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )