Metamath Proof Explorer

Theorem catidd

Description: Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catidd.b ⊢φ→B=BaseC
catidd.h ⊢φ→H=Hom⁡C
catidd.o ⊢φ→·˙=comp⁡C
catidd.c ⊢φ→C∈Cat
catidd.1 ⊢φ∧x∈B→1˙∈xHx
catidd.2 ⊢φ∧x∈B∧y∈B∧f∈yHx→1˙yx·˙xf=f
catidd.3 ⊢φ∧x∈B∧y∈B∧f∈xHy→fxx·˙y1˙=f
Assertion catidd ⊢φ→Id⁡C=x∈B⟼1˙

Proof

Step Hyp Ref Expression
1 catidd.b ⊢φ→B=BaseC
2 catidd.h ⊢φ→H=Hom⁡C
3 catidd.o ⊢φ→·˙=comp⁡C
4 catidd.c ⊢φ→C∈Cat
5 catidd.1 ⊢φ∧x∈B→1˙∈xHx
6 catidd.2 ⊢φ∧x∈B∧y∈B∧f∈yHx→1˙yx·˙xf=f
7 catidd.3 ⊢φ∧x∈B∧y∈B∧f∈xHy→fxx·˙y1˙=f
8 6 ex ⊢φ→x∈B∧y∈B∧f∈yHx→1˙yx·˙xf=f
9 1 eleq2d ⊢φ→x∈B↔x∈BaseC
10 1 eleq2d ⊢φ→y∈B↔y∈BaseC
11 2 oveqd ⊢φ→yHx=yHom⁡Cx
12 11 eleq2d ⊢φ→f∈yHx↔f∈yHom⁡Cx
13 9 10 12 3anbi123d ⊢φ→x∈B∧y∈B∧f∈yHx↔x∈BaseC∧y∈BaseC∧f∈yHom⁡Cx
14 3 oveqd ⊢φ→yx·˙x=yxcomp⁡Cx
15 14 oveqd ⊢φ→1˙yx·˙xf=1˙yxcomp⁡Cxf
16 15 eqeq1d ⊢φ→1˙yx·˙xf=f↔1˙yxcomp⁡Cxf=f
17 8 13 16 3imtr3d ⊢φ→x∈BaseC∧y∈BaseC∧f∈yHom⁡Cx→1˙yxcomp⁡Cxf=f
18 17 3expd ⊢φ→x∈BaseC→y∈BaseC→f∈yHom⁡Cx→1˙yxcomp⁡Cxf=f
19 18 imp41 ⊢φ∧x∈BaseC∧y∈BaseC∧f∈yHom⁡Cx→1˙yxcomp⁡Cxf=f
20 19 ralrimiva ⊢φ∧x∈BaseC∧y∈BaseC→∀f∈yHom⁡Cx1˙yxcomp⁡Cxf=f
21 7 ex ⊢φ→x∈B∧y∈B∧f∈xHy→fxx·˙y1˙=f
22 2 oveqd ⊢φ→xHy=xHom⁡Cy
23 22 eleq2d ⊢φ→f∈xHy↔f∈xHom⁡Cy
24 9 10 23 3anbi123d ⊢φ→x∈B∧y∈B∧f∈xHy↔x∈BaseC∧y∈BaseC∧f∈xHom⁡Cy
25 3 oveqd ⊢φ→xx·˙y=xxcomp⁡Cy
26 25 oveqd ⊢φ→fxx·˙y1˙=fxxcomp⁡Cy1˙
27 26 eqeq1d ⊢φ→fxx·˙y1˙=f↔fxxcomp⁡Cy1˙=f
28 21 24 27 3imtr3d ⊢φ→x∈BaseC∧y∈BaseC∧f∈xHom⁡Cy→fxxcomp⁡Cy1˙=f
29 28 3expd ⊢φ→x∈BaseC→y∈BaseC→f∈xHom⁡Cy→fxxcomp⁡Cy1˙=f
30 29 imp41 ⊢φ∧x∈BaseC∧y∈BaseC∧f∈xHom⁡Cy→fxxcomp⁡Cy1˙=f
31 30 ralrimiva ⊢φ∧x∈BaseC∧y∈BaseC→∀f∈xHom⁡Cyfxxcomp⁡Cy1˙=f
32 20 31 jca ⊢φ∧x∈BaseC∧y∈BaseC→∀f∈yHom⁡Cx1˙yxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cy1˙=f
33 32 ralrimiva ⊢φ∧x∈BaseC→∀y∈BaseC∀f∈yHom⁡Cx1˙yxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cy1˙=f
34 5 ex ⊢φ→x∈B→1˙∈xHx
35 2 oveqd ⊢φ→xHx=xHom⁡Cx
36 35 eleq2d ⊢φ→1˙∈xHx↔1˙∈xHom⁡Cx
37 34 9 36 3imtr3d ⊢φ→x∈BaseC→1˙∈xHom⁡Cx
38 37 imp ⊢φ∧x∈BaseC→1˙∈xHom⁡Cx
39 eqid ⊢BaseC=BaseC
40 eqid ⊢Hom⁡C=Hom⁡C
41 eqid ⊢comp⁡C=comp⁡C
42 4 adantr ⊢φ∧x∈BaseC→C∈Cat
43 simpr ⊢φ∧x∈BaseC→x∈BaseC
44 39 40 41 42 43 catideu ⊢φ∧x∈BaseC→∃!g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f
45 oveq1 ⊢g=1˙→gyxcomp⁡Cxf=1˙yxcomp⁡Cxf
46 45 eqeq1d ⊢g=1˙→gyxcomp⁡Cxf=f↔1˙yxcomp⁡Cxf=f
47 46 ralbidv ⊢g=1˙→∀f∈yHom⁡Cxgyxcomp⁡Cxf=f↔∀f∈yHom⁡Cx1˙yxcomp⁡Cxf=f
48 oveq2 ⊢g=1˙→fxxcomp⁡Cyg=fxxcomp⁡Cy1˙
49 48 eqeq1d ⊢g=1˙→fxxcomp⁡Cyg=f↔fxxcomp⁡Cy1˙=f
50 49 ralbidv ⊢g=1˙→∀f∈xHom⁡Cyfxxcomp⁡Cyg=f↔∀f∈xHom⁡Cyfxxcomp⁡Cy1˙=f
51 47 50 anbi12d ⊢g=1˙→∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f↔∀f∈yHom⁡Cx1˙yxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cy1˙=f
52 51 ralbidv ⊢g=1˙→∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f↔∀y∈BaseC∀f∈yHom⁡Cx1˙yxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cy1˙=f
53 52 riota2 ⊢1˙∈xHom⁡Cx∧∃!g∈xHom⁡Cx∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f→∀y∈BaseC∀f∈yHom⁡Cx1˙yxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cy1˙=f↔ιg∈xHom⁡Cx|∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f=1˙
54 38 44 53 syl2anc ⊢φ∧x∈BaseC→∀y∈BaseC∀f∈yHom⁡Cx1˙yxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cy1˙=f↔ιg∈xHom⁡Cx|∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f=1˙
55 33 54 mpbid ⊢φ∧x∈BaseC→ιg∈xHom⁡Cx|∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f=1˙
56 55 mpteq2dva ⊢φ→x∈BaseC⟼ιg∈xHom⁡Cx|∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f=x∈BaseC⟼1˙
57 eqid ⊢Id⁡C=Id⁡C
58 39 40 41 4 57 cidfval ⊢φ→Id⁡C=x∈BaseC⟼ιg∈xHom⁡Cx|∀y∈BaseC∀f∈yHom⁡Cxgyxcomp⁡Cxf=f∧∀f∈xHom⁡Cyfxxcomp⁡Cyg=f
59 1 mpteq1d ⊢φ→x∈B⟼1˙=x∈BaseC⟼1˙
60 56 58 59 3eqtr4d ⊢φ→Id⁡C=x∈B⟼1˙