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

Metamath Proof Explorer

Theorem idfu1st

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
Assertion idfu1st ⊢ φ → 1 st ⁡ I = I ↾ B

Proof

Step Hyp Ref Expression
1 idfuval.i ⊢ I = id func ⁡ C
2 idfuval.b ⊢ B = Base C
3 idfuval.c ⊢ φ → C ∈ Cat
4 eqid ⊢ Hom ⁡ C = Hom ⁡ C
5 1 2 3 4 idfuval ⊢ φ → I = I ↾ B z ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ z
6 5 fveq2d ⊢ φ → 1 st ⁡ I = 1 st ⁡ I ↾ B z ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ z
7 2 fvexi ⊢ B ∈ V
8 resiexg ⊢ B ∈ V → I ↾ B ∈ V
9 7 8 ax-mp ⊢ I ↾ B ∈ V
10 7 7 xpex ⊢ B × B ∈ V
11 10 mptex ⊢ z ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ z ∈ V
12 9 11 op1st ⊢ 1 st ⁡ I ↾ B z ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ z = I ↾ B
13 6 12 eqtrdi ⊢ φ → 1 st ⁡ I = I ↾ B