Metamath Proof Explorer


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𝑌 ) ) ) )