Metamath Proof Explorer

Theorem idfucl

Description: The identity functor is a functor. Example 3.20(1) of Adamek p. 30. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis idfucl.i ⊢I=idfunc⁡C
Assertion idfucl ⊢C∈Cat→I∈CFuncC

Proof

Step Hyp Ref Expression
1 idfucl.i ⊢I=idfunc⁡C
2 eqid ⊢BaseC=BaseC
3 id ⊢C∈Cat→C∈Cat
4 eqid ⊢Hom⁡C=Hom⁡C
5 1 2 3 4 idfuval ⊢C∈Cat→I=I↾BaseCz∈BaseC×BaseC⟼I↾Hom⁡C⁡z
6 5 fveq2d ⊢C∈Cat→2nd⁡I=2nd⁡I↾BaseCz∈BaseC×BaseC⟼I↾Hom⁡C⁡z
7 fvex ⊢BaseC∈V
8 resiexg ⊢BaseC∈V→I↾BaseC∈V
9 7 8 ax-mp ⊢I↾BaseC∈V
10 7 7 xpex ⊢BaseC×BaseC∈V
11 10 mptex ⊢z∈BaseC×BaseC⟼I↾Hom⁡C⁡z∈V
12 9 11 op2nd ⊢2nd⁡I↾BaseCz∈BaseC×BaseC⟼I↾Hom⁡C⁡z=z∈BaseC×BaseC⟼I↾Hom⁡C⁡z
13 6 12 eqtrdi ⊢C∈Cat→2nd⁡I=z∈BaseC×BaseC⟼I↾Hom⁡C⁡z
14 13 opeq2d ⊢C∈Cat→I↾BaseC2nd⁡I=I↾BaseCz∈BaseC×BaseC⟼I↾Hom⁡C⁡z
15 5 14 eqtr4d ⊢C∈Cat→I=I↾BaseC2nd⁡I
16 f1oi ⊢I↾BaseC:BaseC⟶1-1 ontoBaseC
17 f1of ⊢I↾BaseC:BaseC⟶1-1 ontoBaseC→I↾BaseC:BaseC⟶BaseC
18 16 17 mp1i ⊢C∈Cat→I↾BaseC:BaseC⟶BaseC
19 f1oi ⊢I↾Hom⁡C⁡z:Hom⁡C⁡z⟶1-1 ontoHom⁡C⁡z
20 f1of ⊢I↾Hom⁡C⁡z:Hom⁡C⁡z⟶1-1 ontoHom⁡C⁡z→I↾Hom⁡C⁡z:Hom⁡C⁡z⟶Hom⁡C⁡z
21 19 20 ax-mp ⊢I↾Hom⁡C⁡z:Hom⁡C⁡z⟶Hom⁡C⁡z
22 fvex ⊢Hom⁡C⁡z∈V
23 22 22 elmap ⊢I↾Hom⁡C⁡z∈Hom⁡C⁡zHom⁡C⁡z↔I↾Hom⁡C⁡z:Hom⁡C⁡z⟶Hom⁡C⁡z
24 21 23 mpbir ⊢I↾Hom⁡C⁡z∈Hom⁡C⁡zHom⁡C⁡z
25 xp1st ⊢z∈BaseC×BaseC→1st⁡z∈BaseC
26 25 adantl ⊢C∈Cat∧z∈BaseC×BaseC→1st⁡z∈BaseC
27 fvresi ⊢1st⁡z∈BaseC→I↾BaseC⁡1st⁡z=1st⁡z
28 26 27 syl ⊢C∈Cat∧z∈BaseC×BaseC→I↾BaseC⁡1st⁡z=1st⁡z
29 xp2nd ⊢z∈BaseC×BaseC→2nd⁡z∈BaseC
30 29 adantl ⊢C∈Cat∧z∈BaseC×BaseC→2nd⁡z∈BaseC
31 fvresi ⊢2nd⁡z∈BaseC→I↾BaseC⁡2nd⁡z=2nd⁡z
32 30 31 syl ⊢C∈Cat∧z∈BaseC×BaseC→I↾BaseC⁡2nd⁡z=2nd⁡z
33 28 32 oveq12d ⊢C∈Cat∧z∈BaseC×BaseC→I↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡z=1st⁡zHom⁡C2nd⁡z
34 df-ov ⊢1st⁡zHom⁡C2nd⁡z=Hom⁡C⁡1st⁡z2nd⁡z
35 33 34 eqtrdi ⊢C∈Cat∧z∈BaseC×BaseC→I↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡z=Hom⁡C⁡1st⁡z2nd⁡z
36 1st2nd2 ⊢z∈BaseC×BaseC→z=1st⁡z2nd⁡z
37 36 adantl ⊢C∈Cat∧z∈BaseC×BaseC→z=1st⁡z2nd⁡z
38 37 fveq2d ⊢C∈Cat∧z∈BaseC×BaseC→Hom⁡C⁡z=Hom⁡C⁡1st⁡z2nd⁡z
39 35 38 eqtr4d ⊢C∈Cat∧z∈BaseC×BaseC→I↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡z=Hom⁡C⁡z
40 39 oveq1d ⊢C∈Cat∧z∈BaseC×BaseC→I↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡zHom⁡C⁡z=Hom⁡C⁡zHom⁡C⁡z
41 24 40 eleqtrrid ⊢C∈Cat∧z∈BaseC×BaseC→I↾Hom⁡C⁡z∈I↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡zHom⁡C⁡z
42 41 ralrimiva ⊢C∈Cat→∀z∈BaseC×BaseCI↾Hom⁡C⁡z∈I↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡zHom⁡C⁡z
43 mptelixpg ⊢BaseC×BaseC∈V→z∈BaseC×BaseC⟼I↾Hom⁡C⁡z∈⨉z∈BaseC×BaseCI↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡zHom⁡C⁡z↔∀z∈BaseC×BaseCI↾Hom⁡C⁡z∈I↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡zHom⁡C⁡z
44 10 43 ax-mp ⊢z∈BaseC×BaseC⟼I↾Hom⁡C⁡z∈⨉z∈BaseC×BaseCI↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡zHom⁡C⁡z↔∀z∈BaseC×BaseCI↾Hom⁡C⁡z∈I↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡zHom⁡C⁡z
45 42 44 sylibr ⊢C∈Cat→z∈BaseC×BaseC⟼I↾Hom⁡C⁡z∈⨉z∈BaseC×BaseCI↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡zHom⁡C⁡z
46 13 45 eqeltrd ⊢C∈Cat→2nd⁡I∈⨉z∈BaseC×BaseCI↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡zHom⁡C⁡z
47 eqid ⊢Id⁡C=Id⁡C
48 simpl ⊢C∈Cat∧x∈BaseC→C∈Cat
49 simpr ⊢C∈Cat∧x∈BaseC→x∈BaseC
50 2 4 47 48 49 catidcl ⊢C∈Cat∧x∈BaseC→Id⁡C⁡x∈xHom⁡Cx
51 fvresi ⊢Id⁡C⁡x∈xHom⁡Cx→I↾xHom⁡Cx⁡Id⁡C⁡x=Id⁡C⁡x
52 50 51 syl ⊢C∈Cat∧x∈BaseC→I↾xHom⁡Cx⁡Id⁡C⁡x=Id⁡C⁡x
53 1 2 48 4 49 49 idfu2nd ⊢C∈Cat∧x∈BaseC→x2nd⁡Ix=I↾xHom⁡Cx
54 53 fveq1d ⊢C∈Cat∧x∈BaseC→x2nd⁡Ix⁡Id⁡C⁡x=I↾xHom⁡Cx⁡Id⁡C⁡x
55 fvresi ⊢x∈BaseC→I↾BaseC⁡x=x
56 55 adantl ⊢C∈Cat∧x∈BaseC→I↾BaseC⁡x=x
57 56 fveq2d ⊢C∈Cat∧x∈BaseC→Id⁡C⁡I↾BaseC⁡x=Id⁡C⁡x
58 52 54 57 3eqtr4d ⊢C∈Cat∧x∈BaseC→x2nd⁡Ix⁡Id⁡C⁡x=Id⁡C⁡I↾BaseC⁡x
59 eqid ⊢comp⁡C=comp⁡C
60 48 ad2antrr ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→C∈Cat
61 49 ad2antrr ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→x∈BaseC
62 simplrl ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→y∈BaseC
63 simplrr ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→z∈BaseC
64 simprl ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→f∈xHom⁡Cy
65 simprr ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→g∈yHom⁡Cz
66 2 4 59 60 61 62 63 64 65 catcocl ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→gxycomp⁡Czf∈xHom⁡Cz
67 fvresi ⊢gxycomp⁡Czf∈xHom⁡Cz→I↾xHom⁡Cz⁡gxycomp⁡Czf=gxycomp⁡Czf
68 66 67 syl ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→I↾xHom⁡Cz⁡gxycomp⁡Czf=gxycomp⁡Czf
69 1 2 60 4 61 63 idfu2nd ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→x2nd⁡Iz=I↾xHom⁡Cz
70 69 fveq1d ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→x2nd⁡Iz⁡gxycomp⁡Czf=I↾xHom⁡Cz⁡gxycomp⁡Czf
71 61 55 syl ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→I↾BaseC⁡x=x
72 fvresi ⊢y∈BaseC→I↾BaseC⁡y=y
73 62 72 syl ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→I↾BaseC⁡y=y
74 71 73 opeq12d ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→I↾BaseC⁡xI↾BaseC⁡y=xy
75 fvresi ⊢z∈BaseC→I↾BaseC⁡z=z
76 63 75 syl ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→I↾BaseC⁡z=z
77 74 76 oveq12d ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→I↾BaseC⁡xI↾BaseC⁡ycomp⁡CI↾BaseC⁡z=xycomp⁡Cz
78 1 2 60 4 62 63 65 idfu2 ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→y2nd⁡Iz⁡g=g
79 1 2 60 4 61 62 64 idfu2 ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→x2nd⁡Iy⁡f=f
80 77 78 79 oveq123d ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→y2nd⁡Iz⁡gI↾BaseC⁡xI↾BaseC⁡ycomp⁡CI↾BaseC⁡zx2nd⁡Iy⁡f=gxycomp⁡Czf
81 68 70 80 3eqtr4d ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC∧f∈xHom⁡Cy∧g∈yHom⁡Cz→x2nd⁡Iz⁡gxycomp⁡Czf=y2nd⁡Iz⁡gI↾BaseC⁡xI↾BaseC⁡ycomp⁡CI↾BaseC⁡zx2nd⁡Iy⁡f
82 81 ralrimivva ⊢C∈Cat∧x∈BaseC∧y∈BaseC∧z∈BaseC→∀f∈xHom⁡Cy∀g∈yHom⁡Czx2nd⁡Iz⁡gxycomp⁡Czf=y2nd⁡Iz⁡gI↾BaseC⁡xI↾BaseC⁡ycomp⁡CI↾BaseC⁡zx2nd⁡Iy⁡f
83 82 ralrimivva ⊢C∈Cat∧x∈BaseC→∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czx2nd⁡Iz⁡gxycomp⁡Czf=y2nd⁡Iz⁡gI↾BaseC⁡xI↾BaseC⁡ycomp⁡CI↾BaseC⁡zx2nd⁡Iy⁡f
84 58 83 jca ⊢C∈Cat∧x∈BaseC→x2nd⁡Ix⁡Id⁡C⁡x=Id⁡C⁡I↾BaseC⁡x∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czx2nd⁡Iz⁡gxycomp⁡Czf=y2nd⁡Iz⁡gI↾BaseC⁡xI↾BaseC⁡ycomp⁡CI↾BaseC⁡zx2nd⁡Iy⁡f
85 84 ralrimiva ⊢C∈Cat→∀x∈BaseCx2nd⁡Ix⁡Id⁡C⁡x=Id⁡C⁡I↾BaseC⁡x∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czx2nd⁡Iz⁡gxycomp⁡Czf=y2nd⁡Iz⁡gI↾BaseC⁡xI↾BaseC⁡ycomp⁡CI↾BaseC⁡zx2nd⁡Iy⁡f
86 2 2 4 4 47 47 59 59 3 3 isfunc ⊢C∈Cat→I↾BaseCCFuncC2nd⁡I↔I↾BaseC:BaseC⟶BaseC∧2nd⁡I∈⨉z∈BaseC×BaseCI↾BaseC⁡1st⁡zHom⁡CI↾BaseC⁡2nd⁡zHom⁡C⁡z∧∀x∈BaseCx2nd⁡Ix⁡Id⁡C⁡x=Id⁡C⁡I↾BaseC⁡x∧∀y∈BaseC∀z∈BaseC∀f∈xHom⁡Cy∀g∈yHom⁡Czx2nd⁡Iz⁡gxycomp⁡Czf=y2nd⁡Iz⁡gI↾BaseC⁡xI↾BaseC⁡ycomp⁡CI↾BaseC⁡zx2nd⁡Iy⁡f
87 18 46 85 86 mpbir3and ⊢C∈Cat→I↾BaseCCFuncC2nd⁡I
88 df-br ⊢I↾BaseCCFuncC2nd⁡I↔I↾BaseC2nd⁡I∈CFuncC
89 87 88 sylib ⊢C∈Cat→I↾BaseC2nd⁡I∈CFuncC
90 15 89 eqeltrd ⊢C∈Cat→I∈CFuncC