Definition df-cid 17677

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.)

Assertion

Ref	Expression
df-cid	⊢ Id = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))

Distinct variable group:   𝑏,𝑐,𝑓,𝑔,ℎ,𝑜,𝑥,𝑦

Detailed syntax breakdown of Definition df-cid

Step	Hyp	Ref	Expression
1		ccid 17673	. 2 class Id
2		vc	. . 3 setvar 𝑐
3		ccat 17672	. . 3 class Cat
4		vb	. . . 4 setvar 𝑏
5	2	cv 1532	. . . . 5 class 𝑐
6		cbs 17208	. . . . 5 class Base
7	5, 6	cfv 6553	. . . 4 class (Base‘𝑐)
8		vh	. . . . 5 setvar ℎ
9		chom 17272	. . . . . 6 class Hom
10	5, 9	cfv 6553	. . . . 5 class (Hom ‘𝑐)
11		vo	. . . . . 6 setvar 𝑜
12		cco 17273	. . . . . . 7 class comp
13	5, 12	cfv 6553	. . . . . 6 class (comp‘𝑐)
14		vx	. . . . . . 7 setvar 𝑥
15	4	cv 1532	. . . . . . 7 class 𝑏
16		vg	. . . . . . . . . . . . . 14 setvar 𝑔
17	16	cv 1532	. . . . . . . . . . . . 13 class 𝑔
18		vf	. . . . . . . . . . . . . 14 setvar 𝑓
19	18	cv 1532	. . . . . . . . . . . . 13 class 𝑓
20		vy	. . . . . . . . . . . . . . . 16 setvar 𝑦
21	20	cv 1532	. . . . . . . . . . . . . . 15 class 𝑦
22	14	cv 1532	. . . . . . . . . . . . . . 15 class 𝑥
23	21, 22	cop 4638	. . . . . . . . . . . . . 14 class ⟨𝑦, 𝑥⟩
24	11	cv 1532	. . . . . . . . . . . . . 14 class 𝑜
25	23, 22, 24	co 7423	. . . . . . . . . . . . 13 class (⟨𝑦, 𝑥⟩𝑜𝑥)
26	17, 19, 25	co 7423	. . . . . . . . . . . 12 class (𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓)
27	26, 19	wceq 1533	. . . . . . . . . . 11 wff (𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓
28	8	cv 1532	. . . . . . . . . . . 12 class ℎ
29	21, 22, 28	co 7423	. . . . . . . . . . 11 class (𝑦ℎ𝑥)
30	27, 18, 29	wral 3050	. . . . . . . . . 10 wff ∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓
31	22, 22	cop 4638	. . . . . . . . . . . . . 14 class ⟨𝑥, 𝑥⟩
32	31, 21, 24	co 7423	. . . . . . . . . . . . 13 class (⟨𝑥, 𝑥⟩𝑜𝑦)
33	19, 17, 32	co 7423	. . . . . . . . . . . 12 class (𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔)
34	33, 19	wceq 1533	. . . . . . . . . . 11 wff (𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓
35	22, 21, 28	co 7423	. . . . . . . . . . 11 class (𝑥ℎ𝑦)
36	34, 18, 35	wral 3050	. . . . . . . . . 10 wff ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓
37	30, 36	wa 394	. . . . . . . . 9 wff (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
38	37, 20, 15	wral 3050	. . . . . . . 8 wff ∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
39	22, 22, 28	co 7423	. . . . . . . 8 class (𝑥ℎ𝑥)
40	38, 16, 39	crio 7378	. . . . . . 7 class (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))
41	14, 15, 40	cmpt 5235	. . . . . 6 class (𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
42	11, 13, 41	csb 3891	. . . . 5 class ⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
43	8, 10, 42	csb 3891	. . . 4 class ⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
44	4, 7, 43	csb 3891	. . 3 class ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
45	2, 3, 44	cmpt 5235	. 2 class (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))
46	1, 45	wceq 1533	1 wff Id = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))

This definition is referenced by:  cidfval  17684  cidffn  17686