Metamath Proof Explorer

Definition df-cid

Description: Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Assertion df-cid ⊢Id=c∈Cat⟼⦋Basec/b⦌⦋Hom⁡c/h⦌⦋comp⁡c/o⦌x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccid classId
1 vc setvarc
2 ccat classCat
3 cbs classBase
4 1 cv setvarc
5 4 3 cfv classBasec
6 vb setvarb
7 chom classHom
8 4 7 cfv classHom⁡c
9 vh setvarh
10 cco classcomp
11 4 10 cfv classcomp⁡c
12 vo setvaro
13 vx setvarx
14 6 cv setvarb
15 vg setvarg
16 13 cv setvarx
17 9 cv setvarh
18 16 16 17 co classxhx
19 vy setvary
20 vf setvarf
21 19 cv setvary
22 21 16 17 co classyhx
23 15 cv setvarg
24 21 16 cop classyx
25 12 cv setvaro
26 24 16 25 co classyxox
27 20 cv setvarf
28 23 27 26 co classgyxoxf
29 28 27 wceq wffgyxoxf=f
30 29 20 22 wral wff∀f∈yhxgyxoxf=f
31 16 21 17 co classxhy
32 16 16 cop classxx
33 32 21 25 co classxxoy
34 27 23 33 co classfxxoyg
35 34 27 wceq wfffxxoyg=f
36 35 20 31 wral wff∀f∈xhyfxxoyg=f
37 30 36 wa wff∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f
38 37 19 14 wral wff∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f
39 38 15 18 crio classιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f
40 13 14 39 cmpt classx∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f
41 12 11 40 csb class⦋comp⁡c/o⦌x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f
42 9 8 41 csb class⦋Hom⁡c/h⦌⦋comp⁡c/o⦌x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f
43 6 5 42 csb class⦋Basec/b⦌⦋Hom⁡c/h⦌⦋comp⁡c/o⦌x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f
44 1 2 43 cmpt classc∈Cat⟼⦋Basec/b⦌⦋Hom⁡c/h⦌⦋comp⁡c/o⦌x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f
45 0 44 wceq wffId=c∈Cat⟼⦋Basec/b⦌⦋Hom⁡c/h⦌⦋comp⁡c/o⦌x∈b⟼ιg∈xhx|∀y∈b∀f∈yhxgyxoxf=f∧∀f∈xhyfxxoyg=f