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	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×c ( 𝐷 FuncCat 𝐸 ) )
	xpcfuchom2.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐵 Func 𝐶 ) )
	xpcfuchom2.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐷 Func 𝐸 ) )
	xpcfuchom2.p	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐵 Func 𝐶 ) )
	xpcfuchom2.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝐷 Func 𝐸 ) )
	xpcfuchom2.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
Assertion	xpcfuchom2	⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝑁 ⟩ 𝐾 ⟨ 𝑃 , 𝑄 ⟩ ) = ( ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑃 ) × ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpcfuchom2.t	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×c ( 𝐷 FuncCat 𝐸 ) )
2		xpcfuchom2.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐵 Func 𝐶 ) )
3		xpcfuchom2.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐷 Func 𝐸 ) )
4		xpcfuchom2.p	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐵 Func 𝐶 ) )
5		xpcfuchom2.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝐷 Func 𝐸 ) )
6		xpcfuchom2.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
7		eqid	⊢ ( 𝐵 FuncCat 𝐶 ) = ( 𝐵 FuncCat 𝐶 )
8	7	fucbas	⊢ ( 𝐵 Func 𝐶 ) = ( Base ‘ ( 𝐵 FuncCat 𝐶 ) )
9		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
10	9	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) )
11		eqid	⊢ ( 𝐵 Nat 𝐶 ) = ( 𝐵 Nat 𝐶 )
12	7 11	fuchom	⊢ ( 𝐵 Nat 𝐶 ) = ( Hom ‘ ( 𝐵 FuncCat 𝐶 ) )
13		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
14	9 13	fuchom	⊢ ( 𝐷 Nat 𝐸 ) = ( Hom ‘ ( 𝐷 FuncCat 𝐸 ) )
15	1 8 10 12 14 2 3 4 5 6	xpchom2	⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝑁 ⟩ 𝐾 ⟨ 𝑃 , 𝑄 ⟩ ) = ( ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑃 ) × ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑄 ) ) )