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=\left(B\mathrm{FuncCat}C\right){\times }_c\left(D\mathrm{FuncCat}E\right)$$
	xpcfuchomfval.b	$$⊢A={\mathrm{Base}}_T$$
	xpcfuchomfval.k	$$⊢K=\mathrm{Hom}\left(T\right)$$
	xpcfuchom.x	$$⊢\phi \to X\in A$$
	xpcfuchom.y	$$⊢\phi \to Y\in A$$
Assertion	xpcfuchom	$$⊢\phi \to XKY=\left(1^{st}\left(X\right)\left(B\mathrm{Nat}C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\left(D\mathrm{Nat}E\right)2^{nd}\left(Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpcfucbas.t	$$⊢T=\left(B\mathrm{FuncCat}C\right){\times }_c\left(D\mathrm{FuncCat}E\right)$$
2		xpcfuchomfval.b	$$⊢A={\mathrm{Base}}_T$$
3		xpcfuchomfval.k	$$⊢K=\mathrm{Hom}\left(T\right)$$
4		xpcfuchom.x	$$⊢\phi \to X\in A$$
5		xpcfuchom.y	$$⊢\phi \to Y\in A$$
6		eqid	$$⊢B\mathrm{FuncCat}C=B\mathrm{FuncCat}C$$
7		eqid	$$⊢B\mathrm{Nat}C=B\mathrm{Nat}C$$
8	6 7	fuchom	$$⊢B\mathrm{Nat}C=\mathrm{Hom}\left(B\mathrm{FuncCat}C\right)$$
9		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
10		eqid	$$⊢D\mathrm{Nat}E=D\mathrm{Nat}E$$
11	9 10	fuchom	$$⊢D\mathrm{Nat}E=\mathrm{Hom}\left(D\mathrm{FuncCat}E\right)$$
12	1 2 8 11 3 4 5	xpchom	$$⊢\phi \to XKY=\left(1^{st}\left(X\right)\left(B\mathrm{Nat}C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\left(D\mathrm{Nat}E\right)2^{nd}\left(Y\right)\right)$$