Theorem xpchom

Description: Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpchomfval.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	xpchomfval.y	⊢ 𝐵 = ( Base ‘ 𝑇 )
	xpchomfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	xpchomfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	xpchomfval.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
	xpchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	xpchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	xpchom	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ( ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpchomfval.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		xpchomfval.y	⊢ 𝐵 = ( Base ‘ 𝑇 )
3		xpchomfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		xpchomfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
5		xpchomfval.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
6		xpchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		xpchom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		simpl	⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → 𝑢 = 𝑋 )
9	8	fveq2d	⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑋 ) )
10		simpr	⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → 𝑣 = 𝑌 )
11	10	fveq2d	⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑌 ) )
12	9 11	oveq12d	⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( ( 1st ‘ 𝑢 ) 𝐻 ( 1st ‘ 𝑣 ) ) = ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) )
13	8	fveq2d	⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( 2nd ‘ 𝑢 ) = ( 2nd ‘ 𝑋 ) )
14	10	fveq2d	⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( 2nd ‘ 𝑣 ) = ( 2nd ‘ 𝑌 ) )
15	13 14	oveq12d	⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( ( 2nd ‘ 𝑢 ) 𝐽 ( 2nd ‘ 𝑣 ) ) = ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) )
16	12 15	xpeq12d	⊢ ( ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) → ( ( ( 1st ‘ 𝑢 ) 𝐻 ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) 𝐽 ( 2nd ‘ 𝑣 ) ) ) = ( ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ) )
17	1 2 3 4 5	xpchomfval	⊢ 𝐾 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( ( ( 1st ‘ 𝑢 ) 𝐻 ( 1st ‘ 𝑣 ) ) × ( ( 2nd ‘ 𝑢 ) 𝐽 ( 2nd ‘ 𝑣 ) ) ) )
18		ovex	⊢ ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) ∈ V
19		ovex	⊢ ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ∈ V
20	18 19	xpex	⊢ ( ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ) ∈ V
21	16 17 20	ovmpoa	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐾 𝑌 ) = ( ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ) )
22	6 7 21	syl2anc	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ( ( ( 1st ‘ 𝑋 ) 𝐻 ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) 𝐽 ( 2nd ‘ 𝑌 ) ) ) )