Metamath Proof Explorer

Theorem idfu2nda

Description: Value of the morphism 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
idfu2nda.y ⊢ φ → Y ∈ B
idfu2nda.h ⊢ φ → H = X Hom ⁡ D Y
Assertion idfu2nda ⊢ φ → X 2 nd ⁡ I Y = I ↾ H

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 idfu2nda.y ⊢ φ → Y ∈ B
6 idfu2nda.h ⊢ φ → H = X Hom ⁡ D Y
7 eqid ⊢ Base C = Base C
8 1 2 eqeltrrid ⊢ φ → id func ⁡ C ∈ D Func E
9 idfurcl ⊢ id func ⁡ C ∈ D Func E → C ∈ Cat
10 8 9 syl ⊢ φ → C ∈ Cat
11 eqid ⊢ Hom ⁡ C = Hom ⁡ C
12 1 2 3 idfu1stalem ⊢ φ → B = Base C
13 4 12 eleqtrd ⊢ φ → X ∈ Base C
14 5 12 eleqtrd ⊢ φ → Y ∈ Base C
15 1 7 10 11 13 14 idfu2nd ⊢ φ → X 2 nd ⁡ I Y = I ↾ X Hom ⁡ C Y
16 eqid ⊢ Hom ⁡ D = Hom ⁡ D
17 1 idfucl ⊢ C ∈ Cat → I ∈ C Func C
18 10 17 syl ⊢ φ → I ∈ C Func C
19 18 func1st2nd ⊢ φ → 1 st ⁡ I C Func C 2 nd ⁡ I
20 2 func1st2nd ⊢ φ → 1 st ⁡ I D Func E 2 nd ⁡ I
21 19 20 funchomf ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
22 7 11 16 21 13 14 homfeqval ⊢ φ → X Hom ⁡ C Y = X Hom ⁡ D Y
23 6 22 eqtr4d ⊢ φ → H = X Hom ⁡ C Y
24 23 reseq2d ⊢ φ → I ↾ H = I ↾ X Hom ⁡ C Y
25 15 24 eqtr4d ⊢ φ → X 2 nd ⁡ I Y = I ↾ H