Metamath Proof Explorer


Theorem idfu2nd

Description: Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses idfuval.i I = id func C
idfuval.b B = Base C
idfuval.c φ C Cat
idfuval.h H = Hom C
idfu2nd.x φ X B
idfu2nd.y φ Y B
Assertion idfu2nd φ X 2 nd I Y = I X H Y

Proof

Step Hyp Ref Expression
1 idfuval.i I = id func C
2 idfuval.b B = Base C
3 idfuval.c φ C Cat
4 idfuval.h H = Hom C
5 idfu2nd.x φ X B
6 idfu2nd.y φ Y B
7 df-ov X 2 nd I Y = 2 nd I X Y
8 1 2 3 4 idfuval φ I = I B z B × B I H z
9 8 fveq2d φ 2 nd I = 2 nd I B z B × B I H z
10 2 fvexi B V
11 resiexg B V I B V
12 10 11 ax-mp I B V
13 10 10 xpex B × B V
14 13 mptex z B × B I H z V
15 12 14 op2nd 2 nd I B z B × B I H z = z B × B I H z
16 9 15 eqtrdi φ 2 nd I = z B × B I H z
17 simpr φ z = X Y z = X Y
18 17 fveq2d φ z = X Y H z = H X Y
19 df-ov X H Y = H X Y
20 18 19 eqtr4di φ z = X Y H z = X H Y
21 20 reseq2d φ z = X Y I H z = I X H Y
22 5 6 opelxpd φ X Y B × B
23 ovex X H Y V
24 resiexg X H Y V I X H Y V
25 23 24 mp1i φ I X H Y V
26 16 21 22 25 fvmptd φ 2 nd I X Y = I X H Y
27 7 26 eqtrid φ X 2 nd I Y = I X H Y