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

Metamath Proof Explorer

Theorem idfu1sta

Description: Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypotheses idfu2nda.i ⊢ I = id func ⁡ C
idfu2nda.d ⊢ φ → I ∈ D Func E
idfu2nda.b ⊢ φ → B = Base D
Assertion idfu1sta ⊢ φ → 1 st ⁡ I = I ↾ B

Proof

Step Hyp Ref Expression
1 idfu2nda.i ⊢ I = id func ⁡ C
2 idfu2nda.d ⊢ φ → I ∈ D Func E
3 idfu2nda.b ⊢ φ → B = Base D
4 eqid ⊢ Base C = Base C
5 1 2 eqeltrrid ⊢ φ → id func ⁡ C ∈ D Func E
6 idfurcl ⊢ id func ⁡ C ∈ D Func E → C ∈ Cat
7 5 6 syl ⊢ φ → C ∈ Cat
8 1 4 7 idfu1st ⊢ φ → 1 st ⁡ I = I ↾ Base C
9 1 2 3 idfu1stalem ⊢ φ → B = Base C
10 9 reseq2d ⊢ φ → I ↾ B = I ↾ Base C
11 8 10 eqtr4d ⊢ φ → 1 st ⁡ I = I ↾ B