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

Metamath Proof Explorer

Theorem ucnimalem

Description: Reformulate the G function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Hypotheses ucnprima.1 
|- ( ph -> U e. ( UnifOn ` X ) )
ucnprima.2 
|- ( ph -> V e. ( UnifOn ` Y ) )
ucnprima.3 
|- ( ph -> F e. ( U uCn V ) )
ucnprima.4 
|- ( ph -> W e. V )
ucnprima.5 
|- G = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )
Assertion ucnimalem 
|- G = ( p e. ( X X. X ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )

Proof

Step Hyp Ref Expression
1 ucnprima.1 
 |-  ( ph -> U e. ( UnifOn ` X ) )
2 ucnprima.2 
 |-  ( ph -> V e. ( UnifOn ` Y ) )
3 ucnprima.3 
 |-  ( ph -> F e. ( U uCn V ) )
4 ucnprima.4 
 |-  ( ph -> W e. V )
5 ucnprima.5 
 |-  G = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )
6 vex 
 |-  x e. _V
7 vex 
 |-  y e. _V
8 6 7 op1std 
 |-  ( p = <. x , y >. -> ( 1st ` p ) = x )
9 8 fveq2d 
 |-  ( p = <. x , y >. -> ( F ` ( 1st ` p ) ) = ( F ` x ) )
10 6 7 op2ndd 
 |-  ( p = <. x , y >. -> ( 2nd ` p ) = y )
11 10 fveq2d 
 |-  ( p = <. x , y >. -> ( F ` ( 2nd ` p ) ) = ( F ` y ) )
12 9 11 opeq12d 
 |-  ( p = <. x , y >. -> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. = <. ( F ` x ) , ( F ` y ) >. )
13 12 mpompt 
 |-  ( p e. ( X X. X ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. ) = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )
14 5 13 eqtr4i 
 |-  G = ( p e. ( X X. X ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )