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

Metamath Proof Explorer

Theorem idfu1a

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
idfu2nda.x ⊢ φ → X ∈ B
Assertion idfu1a ⊢ φ → 1 st ⁡ I ⁡ X = X

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 idfu2nda.x ⊢ φ → X ∈ B
5 eqid ⊢ Base C = Base C
6 1 2 eqeltrrid ⊢ φ → id func ⁡ C ∈ D Func E
7 idfurcl ⊢ id func ⁡ C ∈ D Func E → C ∈ Cat
8 6 7 syl ⊢ φ → C ∈ Cat
9 1 2 3 idfu1stalem ⊢ φ → B = Base C
10 4 9 eleqtrd ⊢ φ → X ∈ Base C
11 1 5 8 10 idfu1 ⊢ φ → 1 st ⁡ I ⁡ X = X