Definition df-cid 16798

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 16794	. 2 class Id
2		vc	. . 3 setvar 𝑐
3		ccat 16793	. . 3 class Cat
4		vb	. . . 4 setvar 𝑏
5	2	cv 1506	. . . . 5 class 𝑐
6		cbs 16339	. . . . 5 class Base
7	5, 6	cfv 6188	. . . 4 class (Base‘𝑐)
8		vh	. . . . 5 setvar ℎ
9		chom 16432	. . . . . 6 class Hom
10	5, 9	cfv 6188	. . . . 5 class (Hom ‘𝑐)
11		vo	. . . . . 6 setvar 𝑜
12		cco 16433	. . . . . . 7 class comp
13	5, 12	cfv 6188	. . . . . 6 class (comp‘𝑐)
14		vx	. . . . . . 7 setvar 𝑥
15	4	cv 1506	. . . . . . 7 class 𝑏
16		vg	. . . . . . . . . . . . . 14 setvar 𝑔
17	16	cv 1506	. . . . . . . . . . . . 13 class 𝑔
18		vf	. . . . . . . . . . . . . 14 setvar 𝑓
19	18	cv 1506	. . . . . . . . . . . . 13 class 𝑓
20		vy	. . . . . . . . . . . . . . . 16 setvar 𝑦
21	20	cv 1506	. . . . . . . . . . . . . . 15 class 𝑦
22	14	cv 1506	. . . . . . . . . . . . . . 15 class 𝑥
23	21, 22	cop 4447	. . . . . . . . . . . . . 14 class ⟨𝑦, 𝑥⟩
24	11	cv 1506	. . . . . . . . . . . . . 14 class 𝑜
25	23, 22, 24	co 6976	. . . . . . . . . . . . 13 class (⟨𝑦, 𝑥⟩𝑜𝑥)
26	17, 19, 25	co 6976	. . . . . . . . . . . 12 class (𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓)
27	26, 19	wceq 1507	. . . . . . . . . . 11 wff (𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓
28	8	cv 1506	. . . . . . . . . . . 12 class ℎ
29	21, 22, 28	co 6976	. . . . . . . . . . 11 class (𝑦ℎ𝑥)
30	27, 18, 29	wral 3088	. . . . . . . . . 10 wff ∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓
31	22, 22	cop 4447	. . . . . . . . . . . . . 14 class ⟨𝑥, 𝑥⟩
32	31, 21, 24	co 6976	. . . . . . . . . . . . 13 class (⟨𝑥, 𝑥⟩𝑜𝑦)
33	19, 17, 32	co 6976	. . . . . . . . . . . 12 class (𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔)
34	33, 19	wceq 1507	. . . . . . . . . . 11 wff (𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓
35	22, 21, 28	co 6976	. . . . . . . . . . 11 class (𝑥ℎ𝑦)
36	34, 18, 35	wral 3088	. . . . . . . . . 10 wff ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓
37	30, 36	wa 387	. . . . . . . . 9 wff (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
38	37, 20, 15	wral 3088	. . . . . . . 8 wff ∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
39	22, 22, 28	co 6976	. . . . . . . 8 class (𝑥ℎ𝑥)
40	38, 16, 39	crio 6936	. . . . . . 7 class (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))
41	14, 15, 40	cmpt 5008	. . . . . 6 class (𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
42	11, 13, 41	csb 3786	. . . . 5 class ⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
43	8, 10, 42	csb 3786	. . . 4 class ⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
44	4, 7, 43	csb 3786	. . 3 class ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
45	2, 3, 44	cmpt 5008	. 2 class (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))
46	1, 45	wceq 1507	1 wff Id = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))

This definition is referenced by:  cidfval  16805  cidffn  16807