Theorem prf2

Description: Value of the pairing functor on morphisms. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	prfval.k	|- P = ( F pairF G )
	prfval.b	|- B = ( Base ` C )
	prfval.h	|- H = ( Hom ` C )
	prfval.c	|- ( ph -> F e. ( C Func D ) )
	prfval.d	|- ( ph -> G e. ( C Func E ) )
	prf1.x	|- ( ph -> X e. B )
	prf2.y	|- ( ph -> Y e. B )
	prf2.k	|- ( ph -> K e. ( X H Y ) )
Assertion	prf2	|- ( ph -> ( ( X ( 2nd ` P ) Y ) ` K ) = <. ( ( X ( 2nd ` F ) Y ) ` K ) , ( ( X ( 2nd ` G ) Y ) ` K ) >. )

Proof

Step	Hyp	Ref	Expression
1		prfval.k	|- P = ( F pairF G )
2		prfval.b	|- B = ( Base ` C )
3		prfval.h	|- H = ( Hom ` C )
4		prfval.c	|- ( ph -> F e. ( C Func D ) )
5		prfval.d	|- ( ph -> G e. ( C Func E ) )
6		prf1.x	|- ( ph -> X e. B )
7		prf2.y	|- ( ph -> Y e. B )
8		prf2.k	|- ( ph -> K e. ( X H Y ) )
9	1 2 3 4 5 6 7	prf2fval	|- ( ph -> ( X ( 2nd ` P ) Y ) = ( h e. ( X H Y ) |-> <. ( ( X ( 2nd ` F ) Y ) ` h ) , ( ( X ( 2nd ` G ) Y ) ` h ) >. ) )
10		simpr	|- ( ( ph /\ h = K ) -> h = K )
11	10	fveq2d	|- ( ( ph /\ h = K ) -> ( ( X ( 2nd ` F ) Y ) ` h ) = ( ( X ( 2nd ` F ) Y ) ` K ) )
12	10	fveq2d	|- ( ( ph /\ h = K ) -> ( ( X ( 2nd ` G ) Y ) ` h ) = ( ( X ( 2nd ` G ) Y ) ` K ) )
13	11 12	opeq12d	|- ( ( ph /\ h = K ) -> <. ( ( X ( 2nd ` F ) Y ) ` h ) , ( ( X ( 2nd ` G ) Y ) ` h ) >. = <. ( ( X ( 2nd ` F ) Y ) ` K ) , ( ( X ( 2nd ` G ) Y ) ` K ) >. )
14		opex	|- <. ( ( X ( 2nd ` F ) Y ) ` K ) , ( ( X ( 2nd ` G ) Y ) ` K ) >. e. _V
15	14	a1i	|- ( ph -> <. ( ( X ( 2nd ` F ) Y ) ` K ) , ( ( X ( 2nd ` G ) Y ) ` K ) >. e. _V )
16	9 13 8 15	fvmptd	|- ( ph -> ( ( X ( 2nd ` P ) Y ) ` K ) = <. ( ( X ( 2nd ` F ) Y ) ` K ) , ( ( X ( 2nd ` G ) Y ) ` K ) >. )