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 ⟼ ⦋ Base c / b⦌ ⦋ Hom ⁡ c / h⦌ ⦋ comp ⁡ c / o⦌ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccid class Id
1 vc setvar c
2 ccat class Cat
3 cbs class Base
4 1 cv setvar c
5 4 3 cfv class Base c
6 vb setvar b
7 chom class Hom
8 4 7 cfv class Hom ⁡ c
9 vh setvar h
10 cco class comp
11 4 10 cfv class comp ⁡ c
12 vo setvar o
13 vx setvar x
14 6 cv setvar b
15 vg setvar g
16 13 cv setvar x
17 9 cv setvar h
18 16 16 17 co class x h x
19 vy setvar y
20 vf setvar f
21 19 cv setvar y
22 21 16 17 co class y h x
23 15 cv setvar g
24 21 16 cop class y x
25 12 cv setvar o
26 24 16 25 co class y x o x
27 20 cv setvar f
28 23 27 26 co class g y x o x f
29 28 27 wceq wff g y x o x f = f
30 29 20 22 wral wff ∀ f ∈ y h x g y x o x f = f
31 16 21 17 co class x h y
32 16 16 cop class x x
33 32 21 25 co class x x o y
34 27 23 33 co class f x x o y g
35 34 27 wceq wff f x x o y g = f
36 35 20 31 wral wff ∀ f ∈ x h y f x x o y g = f
37 30 36 wa wff ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
38 37 19 14 wral wff ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
39 38 15 18 crio class ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
40 13 14 39 cmpt class x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
41 12 11 40 csb class ⦋ comp ⁡ c / o⦌ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
42 9 8 41 csb class ⦋ Hom ⁡ c / h⦌ ⦋ comp ⁡ c / o⦌ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
43 6 5 42 csb class ⦋ Base c / b⦌ ⦋ Hom ⁡ c / h⦌ ⦋ comp ⁡ c / o⦌ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
44 1 2 43 cmpt class c ∈ Cat ⟼ ⦋ Base c / b⦌ ⦋ Hom ⁡ c / h⦌ ⦋ comp ⁡ c / o⦌ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f
45 0 44 wceq wff Id = c ∈ Cat ⟼ ⦋ Base c / b⦌ ⦋ Hom ⁡ c / h⦌ ⦋ comp ⁡ c / o⦌ x ∈ b ⟼ ι g ∈ x h x | ∀ y ∈ b ∀ f ∈ y h x g y x o x f = f ∧ ∀ f ∈ x h y f x x o y g = f