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

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