# Metamath Proof Explorer

## Theorem idfu1

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

Ref Expression
Hypotheses idfuval.i ${⊢}{I}={id}_{\mathrm{func}}\left({C}\right)$
idfuval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
idfuval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
idfu1.x ${⊢}{\phi }\to {X}\in {B}$
Assertion idfu1 ${⊢}{\phi }\to {1}^{st}\left({I}\right)\left({X}\right)={X}$

### Proof

Step Hyp Ref Expression
1 idfuval.i ${⊢}{I}={id}_{\mathrm{func}}\left({C}\right)$
2 idfuval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 idfuval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
4 idfu1.x ${⊢}{\phi }\to {X}\in {B}$
5 1 2 3 idfu1st ${⊢}{\phi }\to {1}^{st}\left({I}\right)={\mathrm{I}↾}_{{B}}$
6 5 fveq1d ${⊢}{\phi }\to {1}^{st}\left({I}\right)\left({X}\right)=\left({\mathrm{I}↾}_{{B}}\right)\left({X}\right)$
7 fvresi ${⊢}{X}\in {B}\to \left({\mathrm{I}↾}_{{B}}\right)\left({X}\right)={X}$
8 4 7 syl ${⊢}{\phi }\to \left({\mathrm{I}↾}_{{B}}\right)\left({X}\right)={X}$
9 6 8 eqtrd ${⊢}{\phi }\to {1}^{st}\left({I}\right)\left({X}\right)={X}$