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