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=idfuncC
idfuval.b B=BaseC
idfuval.c φCCat
idfuval.h H=HomC
idfu2nd.x φXB
idfu2nd.y φYB
idfu2.f φFXHY
Assertion idfu2 φX2ndIYF=F

Proof

Step Hyp Ref Expression
1 idfuval.i I=idfuncC
2 idfuval.b B=BaseC
3 idfuval.c φCCat
4 idfuval.h H=HomC
5 idfu2nd.x φXB
6 idfu2nd.y φYB
7 idfu2.f φFXHY
8 1 2 3 4 5 6 idfu2nd φX2ndIY=IXHY
9 8 fveq1d φX2ndIYF=IXHYF
10 fvresi FXHYIXHYF=F
11 7 10 syl φIXHYF=F
12 9 11 eqtrd φX2ndIYF=F