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	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×_c ( 𝐷 FuncCat 𝐸 ) )
	xpcfuchomfval.b	⊢ 𝐴 = ( Base ‘ 𝑇 )
	xpcfuchomfval.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
	xpcfuchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	xpcfuchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
Assertion	xpcfuchom	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ( ( ( 1^st ‘ 𝑋 ) ( 𝐵 Nat 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( 2^nd ‘ 𝑌 ) ) ) )

Step	Hyp	Ref	Expression
1		xpcfucbas.t	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×_c ( 𝐷 FuncCat 𝐸 ) )
2		xpcfuchomfval.b	⊢ 𝐴 = ( Base ‘ 𝑇 )
3		xpcfuchomfval.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
4		xpcfuchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
5		xpcfuchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
6		eqid	⊢ ( 𝐵 FuncCat 𝐶 ) = ( 𝐵 FuncCat 𝐶 )
7		eqid	⊢ ( 𝐵 Nat 𝐶 ) = ( 𝐵 Nat 𝐶 )
8	6 7	fuchom	⊢ ( 𝐵 Nat 𝐶 ) = ( Hom ‘ ( 𝐵 FuncCat 𝐶 ) )
9		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
10		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
11	9 10	fuchom	⊢ ( 𝐷 Nat 𝐸 ) = ( Hom ‘ ( 𝐷 FuncCat 𝐸 ) )
12	1 2 8 11 3 4 5	xpchom	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ( ( ( 1^st ‘ 𝑋 ) ( 𝐵 Nat 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( 2^nd ‘ 𝑌 ) ) ) )

Metamath Proof Explorer