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

Metamath Proof Explorer

Theorem ussval

Description: The uniform structure on uniform space W . This proof uses a trick with fvprc to avoid requiring W to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017)

Ref Expression
Hypotheses ussval.1 
|- B = ( Base ` W )
ussval.2 
|- U = ( UnifSet ` W )
Assertion ussval 
|- ( U |`t ( B X. B ) ) = ( UnifSt ` W )

Proof

Step Hyp Ref Expression
1 ussval.1 
 |-  B = ( Base ` W )
2 ussval.2 
 |-  U = ( UnifSet ` W )
3 1 1 xpeq12i 
 |-  ( B X. B ) = ( ( Base ` W ) X. ( Base ` W ) )
4 2 3 oveq12i 
 |-  ( U |`t ( B X. B ) ) = ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) )
5 fveq2 
 |-  ( w = W -> ( UnifSet ` w ) = ( UnifSet ` W ) )
6 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
7 6 sqxpeqd 
 |-  ( w = W -> ( ( Base ` w ) X. ( Base ` w ) ) = ( ( Base ` W ) X. ( Base ` W ) ) )
8 5 7 oveq12d 
 |-  ( w = W -> ( ( UnifSet ` w ) |`t ( ( Base ` w ) X. ( Base ` w ) ) ) = ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) )
9 df-uss 
 |-  UnifSt = ( w e. _V |-> ( ( UnifSet ` w ) |`t ( ( Base ` w ) X. ( Base ` w ) ) ) )
10 ovex 
 |-  ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) e. _V
11 8 9 10 fvmpt 
 |-  ( W e. _V -> ( UnifSt ` W ) = ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) )
12 4 11 eqtr4id 
 |-  ( W e. _V -> ( U |`t ( B X. B ) ) = ( UnifSt ` W ) )
13 0rest 
 |-  ( (/) |`t ( B X. B ) ) = (/)
14 fvprc 
 |-  ( -. W e. _V -> ( UnifSet ` W ) = (/) )
15 2 14 eqtrid 
 |-  ( -. W e. _V -> U = (/) )
16 15 oveq1d 
 |-  ( -. W e. _V -> ( U |`t ( B X. B ) ) = ( (/) |`t ( B X. B ) ) )
17 fvprc 
 |-  ( -. W e. _V -> ( UnifSt ` W ) = (/) )
18 13 16 17 3eqtr4a 
 |-  ( -. W e. _V -> ( U |`t ( B X. B ) ) = ( UnifSt ` W ) )
19 12 18 pm2.61i 
 |-  ( U |`t ( B X. B ) ) = ( UnifSt ` W )