Metamath Proof Explorer


Theorem funcf2

Description: The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses funcixp.b B = Base D
funcixp.h H = Hom D
funcixp.j J = Hom E
funcixp.f φ F D Func E G
funcf2.x φ X B
funcf2.y φ Y B
Assertion funcf2 φ X G Y : X H Y F X J F Y

Proof

Step Hyp Ref Expression
1 funcixp.b B = Base D
2 funcixp.h H = Hom D
3 funcixp.j J = Hom E
4 funcixp.f φ F D Func E G
5 funcf2.x φ X B
6 funcf2.y φ Y B
7 df-ov X G Y = G X Y
8 1 2 3 4 funcixp φ G z B × B F 1 st z J F 2 nd z H z
9 5 6 opelxpd φ X Y B × B
10 2fveq3 z = X Y F 1 st z = F 1 st X Y
11 2fveq3 z = X Y F 2 nd z = F 2 nd X Y
12 10 11 oveq12d z = X Y F 1 st z J F 2 nd z = F 1 st X Y J F 2 nd X Y
13 fveq2 z = X Y H z = H X Y
14 df-ov X H Y = H X Y
15 13 14 syl6eqr z = X Y H z = X H Y
16 12 15 oveq12d z = X Y F 1 st z J F 2 nd z H z = F 1 st X Y J F 2 nd X Y X H Y
17 16 fvixp G z B × B F 1 st z J F 2 nd z H z X Y B × B G X Y F 1 st X Y J F 2 nd X Y X H Y
18 8 9 17 syl2anc φ G X Y F 1 st X Y J F 2 nd X Y X H Y
19 7 18 eqeltrid φ X G Y F 1 st X Y J F 2 nd X Y X H Y
20 op1stg X B Y B 1 st X Y = X
21 20 fveq2d X B Y B F 1 st X Y = F X
22 op2ndg X B Y B 2 nd X Y = Y
23 22 fveq2d X B Y B F 2 nd X Y = F Y
24 21 23 oveq12d X B Y B F 1 st X Y J F 2 nd X Y = F X J F Y
25 5 6 24 syl2anc φ F 1 st X Y J F 2 nd X Y = F X J F Y
26 25 oveq1d φ F 1 st X Y J F 2 nd X Y X H Y = F X J F Y X H Y
27 19 26 eleqtrd φ X G Y F X J F Y X H Y
28 elmapi X G Y F X J F Y X H Y X G Y : X H Y F X J F Y
29 27 28 syl φ X G Y : X H Y F X J F Y