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=\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)$$
Assertion	xpcfuchomfval	$$⊢K=\left(u\in A,v\in A⟼\left(1^{st}\left(u\right)\left(B\mathrm{Nat}C\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\left(D\mathrm{Nat}E\right)2^{nd}\left(v\right)\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		eqid	$$⊢B\mathrm{FuncCat}C=B\mathrm{FuncCat}C$$
5		eqid	$$⊢B\mathrm{Nat}C=B\mathrm{Nat}C$$
6	4 5	fuchom	$$⊢B\mathrm{Nat}C=\mathrm{Hom}\left(B\mathrm{FuncCat}C\right)$$
7		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
8		eqid	$$⊢D\mathrm{Nat}E=D\mathrm{Nat}E$$
9	7 8	fuchom	$$⊢D\mathrm{Nat}E=\mathrm{Hom}\left(D\mathrm{FuncCat}E\right)$$
10	1 2 6 9 3	xpchomfval	$$⊢K=\left(u\in A,v\in A⟼\left(1^{st}\left(u\right)\left(B\mathrm{Nat}C\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\left(D\mathrm{Nat}E\right)2^{nd}\left(v\right)\right)\right)$$