Theorem xpcfuchomfval

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 )
Assertion	xpcfuchomfval	|- K = ( u e. A , v e. A |-> ( ( ( 1st ` u ) ( B Nat C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( D Nat E ) ( 2nd ` v ) ) ) )

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		eqid	|- ( B FuncCat C ) = ( B FuncCat C )
5		eqid	|- ( B Nat C ) = ( B Nat C )
6	4 5	fuchom	|- ( B Nat C ) = ( Hom ` ( B FuncCat C ) )
7		eqid	|- ( D FuncCat E ) = ( D FuncCat E )
8		eqid	|- ( D Nat E ) = ( D Nat E )
9	7 8	fuchom	|- ( D Nat E ) = ( Hom ` ( D FuncCat E ) )
10	1 2 6 9 3	xpchomfval	|- K = ( u e. A , v e. A |-> ( ( ( 1st ` u ) ( B Nat C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( D Nat E ) ( 2nd ` v ) ) ) )