This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem topnval

Description: Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses topnval.1 
|- B = ( Base ` W )
topnval.2 
|- J = ( TopSet ` W )
Assertion topnval 
|- ( J |`t B ) = ( TopOpen ` W )

Proof

Step Hyp Ref Expression
1 topnval.1 
 |-  B = ( Base ` W )
2 topnval.2 
 |-  J = ( TopSet ` W )
3 fveq2 
 |-  ( w = W -> ( TopSet ` w ) = ( TopSet ` W ) )
4 3 2 eqtr4di 
 |-  ( w = W -> ( TopSet ` w ) = J )
5 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
6 5 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = B )
7 4 6 oveq12d 
 |-  ( w = W -> ( ( TopSet ` w ) |`t ( Base ` w ) ) = ( J |`t B ) )
8 df-topn 
 |-  TopOpen = ( w e. _V |-> ( ( TopSet ` w ) |`t ( Base ` w ) ) )
9 ovex 
 |-  ( J |`t B ) e. _V
10 7 8 9 fvmpt 
 |-  ( W e. _V -> ( TopOpen ` W ) = ( J |`t B ) )
11 10 eqcomd 
 |-  ( W e. _V -> ( J |`t B ) = ( TopOpen ` W ) )
12 0rest 
 |-  ( (/) |`t B ) = (/)
13 fvprc 
 |-  ( -. W e. _V -> ( TopSet ` W ) = (/) )
14 2 13 eqtrid 
 |-  ( -. W e. _V -> J = (/) )
15 14 oveq1d 
 |-  ( -. W e. _V -> ( J |`t B ) = ( (/) |`t B ) )
16 fvprc 
 |-  ( -. W e. _V -> ( TopOpen ` W ) = (/) )
17 12 15 16 3eqtr4a 
 |-  ( -. W e. _V -> ( J |`t B ) = ( TopOpen ` W ) )
18 11 17 pm2.61i 
 |-  ( J |`t B ) = ( TopOpen ` W )