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 ) )