Theorem xpcfuchom

Description: Set of morphisms of the binary product of categories of functors. (Contributed by Zhi Wang, 1-Oct-2025)

	Ref	Expression
Hypotheses	xpcfucbas.t	|- T = ( ( B FuncCat C ) Xc. ( D FuncCat E ) )
	xpcfuchomfval.b	|- A = ( Base ` T )
	xpcfuchomfval.k	|- K = ( Hom ` T )
	xpcfuchom.x	|- ( ph -> X e. A )
	xpcfuchom.y	|- ( ph -> Y e. A )
Assertion	xpcfuchom	|- ( ph -> ( X K Y ) = ( ( ( 1st ` X ) ( B Nat C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( D Nat E ) ( 2nd ` Y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpcfucbas.t	|- T = ( ( B FuncCat C ) Xc. ( D FuncCat E ) )
2		xpcfuchomfval.b	|- A = ( Base ` T )
3		xpcfuchomfval.k	|- K = ( Hom ` T )
4		xpcfuchom.x	|- ( ph -> X e. A )
5		xpcfuchom.y	|- ( ph -> Y e. A )
6		eqid	|- ( B FuncCat C ) = ( B FuncCat C )
7		eqid	|- ( B Nat C ) = ( B Nat C )
8	6 7	fuchom	|- ( B Nat C ) = ( Hom ` ( B FuncCat C ) )
9		eqid	|- ( D FuncCat E ) = ( D FuncCat E )
10		eqid	|- ( D Nat E ) = ( D Nat E )
11	9 10	fuchom	|- ( D Nat E ) = ( Hom ` ( D FuncCat E ) )
12	1 2 8 11 3 4 5	xpchom	|- ( ph -> ( X K Y ) = ( ( ( 1st ` X ) ( B Nat C ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( D Nat E ) ( 2nd ` Y ) ) ) )