Metamath Proof Explorer


Theorem idfu2

Description: Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-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
idfu2.f φ F X H Y
Assertion idfu2 φ X 2 nd I Y F = F

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 idfu2.f φ F X H Y
8 1 2 3 4 5 6 idfu2nd φ X 2 nd I Y = I X H Y
9 8 fveq1d φ X 2 nd I Y F = I X H Y F
10 fvresi F X H Y I X H Y F = F
11 7 10 syl φ I X H Y F = F
12 9 11 eqtrd φ X 2 nd I Y F = F