This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 func ⁡ C
idfuval.b ⊢ B = Base C
idfuval.c ⊢ φ → C ∈ Cat
idfu1.x ⊢ φ → X ∈ B
Assertion idfu1 ⊢ φ → 1 st ⁡ I ⁡ X = X

Proof

Step Hyp Ref Expression
1 idfuval.i ⊢ I = id func ⁡ C
2 idfuval.b ⊢ B = Base C
3 idfuval.c ⊢ φ → C ∈ Cat
4 idfu1.x ⊢ φ → X ∈ B
5 1 2 3 idfu1st ⊢ φ → 1 st ⁡ I = I ↾ B
6 5 fveq1d ⊢ φ → 1 st ⁡ I ⁡ X = I ↾ B ⁡ X
7 fvresi ⊢ X ∈ B → I ↾ B ⁡ X = X
8 4 7 syl ⊢ φ → I ↾ B ⁡ X = X
9 6 8 eqtrd ⊢ φ → 1 st ⁡ I ⁡ X = X