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	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×_c ( 𝐷 FuncCat 𝐸 ) )
	xpcfuchomfval.b	⊢ 𝐴 = ( Base ‘ 𝑇 )
	xpcfuchomfval.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
Assertion	xpcfuchomfval	⊢ 𝐾 = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐴 ↦ ( ( ( 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		eqid	⊢ ( 𝐵 FuncCat 𝐶 ) = ( 𝐵 FuncCat 𝐶 )
5		eqid	⊢ ( 𝐵 Nat 𝐶 ) = ( 𝐵 Nat 𝐶 )
6	4 5	fuchom	⊢ ( 𝐵 Nat 𝐶 ) = ( Hom ‘ ( 𝐵 FuncCat 𝐶 ) )
7		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
8		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
9	7 8	fuchom	⊢ ( 𝐷 Nat 𝐸 ) = ( Hom ‘ ( 𝐷 FuncCat 𝐸 ) )
10	1 2 6 9 3	xpchomfval	⊢ 𝐾 = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ 𝐴 ↦ ( ( ( 1^st ‘ 𝑢 ) ( 𝐵 Nat 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 2^nd ‘ 𝑣 ) ) ) )

Metamath Proof Explorer