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