Theorem xpcfuchom2

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

	Ref	Expression
Hypotheses	xpcfuchom2.t	|- T = ( ( B FuncCat C ) Xc. ( D FuncCat E ) )
	xpcfuchom2.m	|- ( ph -> M e. ( B Func C ) )
	xpcfuchom2.n	|- ( ph -> N e. ( D Func E ) )
	xpcfuchom2.p	|- ( ph -> P e. ( B Func C ) )
	xpcfuchom2.q	|- ( ph -> Q e. ( D Func E ) )
	xpcfuchom2.k	|- K = ( Hom ` T )
Assertion	xpcfuchom2	|- ( ph -> ( <. M , N >. K <. P , Q >. ) = ( ( M ( B Nat C ) P ) X. ( N ( D Nat E ) Q ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpcfuchom2.t	|- T = ( ( B FuncCat C ) Xc. ( D FuncCat E ) )
2		xpcfuchom2.m	|- ( ph -> M e. ( B Func C ) )
3		xpcfuchom2.n	|- ( ph -> N e. ( D Func E ) )
4		xpcfuchom2.p	|- ( ph -> P e. ( B Func C ) )
5		xpcfuchom2.q	|- ( ph -> Q e. ( D Func E ) )
6		xpcfuchom2.k	|- K = ( Hom ` T )
7		eqid	|- ( B FuncCat C ) = ( B FuncCat C )
8	7	fucbas	|- ( B Func C ) = ( Base ` ( B FuncCat C ) )
9		eqid	|- ( D FuncCat E ) = ( D FuncCat E )
10	9	fucbas	|- ( D Func E ) = ( Base ` ( D FuncCat E ) )
11		eqid	|- ( B Nat C ) = ( B Nat C )
12	7 11	fuchom	|- ( B Nat C ) = ( Hom ` ( B FuncCat C ) )
13		eqid	|- ( D Nat E ) = ( D Nat E )
14	9 13	fuchom	|- ( D Nat E ) = ( Hom ` ( D FuncCat E ) )
15	1 8 10 12 14 2 3 4 5 6	xpchom2	|- ( ph -> ( <. M , N >. K <. P , Q >. ) = ( ( M ( B Nat C ) P ) X. ( N ( D Nat E ) Q ) ) )