Metamath Proof Explorer

Theorem idfuval

Description: Value of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses idfuval.i ⊢I=idfunc⁡C
idfuval.b ⊢B=BaseC
idfuval.c ⊢φ→C∈Cat
idfuval.h ⊢H=Hom⁡C
Assertion idfuval ⊢φ→I=I↾Bz∈B×B⟼I↾H⁡z

Proof

Step Hyp Ref Expression
1 idfuval.i ⊢I=idfunc⁡C
2 idfuval.b ⊢B=BaseC
3 idfuval.c ⊢φ→C∈Cat
4 idfuval.h ⊢H=Hom⁡C
5 fvexd ⊢c=C→Basec∈V
6 fveq2 ⊢c=C→Basec=BaseC
7 6 2 eqtr4di ⊢c=C→Basec=B
8 simpr ⊢c=C∧b=B→b=B
9 8 reseq2d ⊢c=C∧b=B→I↾b=I↾B
10 8 sqxpeqd ⊢c=C∧b=B→b×b=B×B
11 simpl ⊢c=C∧b=B→c=C
12 11 fveq2d ⊢c=C∧b=B→Hom⁡c=Hom⁡C
13 12 4 eqtr4di ⊢c=C∧b=B→Hom⁡c=H
14 13 fveq1d ⊢c=C∧b=B→Hom⁡c⁡z=H⁡z
15 14 reseq2d ⊢c=C∧b=B→I↾Hom⁡c⁡z=I↾H⁡z
16 10 15 mpteq12dv ⊢c=C∧b=B→z∈b×b⟼I↾Hom⁡c⁡z=z∈B×B⟼I↾H⁡z
17 9 16 opeq12d ⊢c=C∧b=B→I↾bz∈b×b⟼I↾Hom⁡c⁡z=I↾Bz∈B×B⟼I↾H⁡z
18 5 7 17 csbied2 ⊢c=C→⦋Basec/b⦌I↾bz∈b×b⟼I↾Hom⁡c⁡z=I↾Bz∈B×B⟼I↾H⁡z
19 df-idfu ⊢idfunc=c∈Cat⟼⦋Basec/b⦌I↾bz∈b×b⟼I↾Hom⁡c⁡z
20 opex ⊢I↾Bz∈B×B⟼I↾H⁡z∈V
21 18 19 20 fvmpt ⊢C∈Cat→idfunc⁡C=I↾Bz∈B×B⟼I↾H⁡z
22 3 21 syl ⊢φ→idfunc⁡C=I↾Bz∈B×B⟼I↾H⁡z
23 1 22 eqtrid ⊢φ→I=I↾Bz∈B×B⟼I↾H⁡z