Definition df-cid 17604

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 17600	. 2 class Id
2		vc	. . 3 setvar 𝑐
3		ccat 17599	. . 3 class Cat
4		vb	. . . 4 setvar 𝑏
5	2	cv 1541	. . . . 5 class 𝑐
6		cbs 17148	. . . . 5 class Base
7	5, 6	cfv 6500	. . . 4 class (Base‘𝑐)
8		vh	. . . . 5 setvar ℎ
9		chom 17200	. . . . . 6 class Hom
10	5, 9	cfv 6500	. . . . 5 class (Hom ‘𝑐)
11		vo	. . . . . 6 setvar 𝑜
12		cco 17201	. . . . . . 7 class comp
13	5, 12	cfv 6500	. . . . . 6 class (comp‘𝑐)
14		vx	. . . . . . 7 setvar 𝑥
15	4	cv 1541	. . . . . . 7 class 𝑏
16		vg	. . . . . . . . . . . . . 14 setvar 𝑔
17	16	cv 1541	. . . . . . . . . . . . 13 class 𝑔
18		vf	. . . . . . . . . . . . . 14 setvar 𝑓
19	18	cv 1541	. . . . . . . . . . . . 13 class 𝑓
20		vy	. . . . . . . . . . . . . . . 16 setvar 𝑦
21	20	cv 1541	. . . . . . . . . . . . . . 15 class 𝑦
22	14	cv 1541	. . . . . . . . . . . . . . 15 class 𝑥
23	21, 22	cop 4588	. . . . . . . . . . . . . 14 class ⟨𝑦, 𝑥⟩
24	11	cv 1541	. . . . . . . . . . . . . 14 class 𝑜
25	23, 22, 24	co 7368	. . . . . . . . . . . . 13 class (⟨𝑦, 𝑥⟩𝑜𝑥)
26	17, 19, 25	co 7368	. . . . . . . . . . . 12 class (𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓)
27	26, 19	wceq 1542	. . . . . . . . . . 11 wff (𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓
28	8	cv 1541	. . . . . . . . . . . 12 class ℎ
29	21, 22, 28	co 7368	. . . . . . . . . . 11 class (𝑦ℎ𝑥)
30	27, 18, 29	wral 3052	. . . . . . . . . 10 wff ∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓
31	22, 22	cop 4588	. . . . . . . . . . . . . 14 class ⟨𝑥, 𝑥⟩
32	31, 21, 24	co 7368	. . . . . . . . . . . . 13 class (⟨𝑥, 𝑥⟩𝑜𝑦)
33	19, 17, 32	co 7368	. . . . . . . . . . . 12 class (𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔)
34	33, 19	wceq 1542	. . . . . . . . . . 11 wff (𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓
35	22, 21, 28	co 7368	. . . . . . . . . . 11 class (𝑥ℎ𝑦)
36	34, 18, 35	wral 3052	. . . . . . . . . 10 wff ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓
37	30, 36	wa 395	. . . . . . . . 9 wff (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
38	37, 20, 15	wral 3052	. . . . . . . 8 wff ∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
39	22, 22, 28	co 7368	. . . . . . . 8 class (𝑥ℎ𝑥)
40	38, 16, 39	crio 7324	. . . . . . 7 class (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))
41	14, 15, 40	cmpt 5181	. . . . . 6 class (𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
42	11, 13, 41	csb 3851	. . . . 5 class ⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
43	8, 10, 42	csb 3851	. . . 4 class ⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
44	4, 7, 43	csb 3851	. . 3 class ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
45	2, 3, 44	cmpt 5181	. 2 class (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))
46	1, 45	wceq 1542	1 wff Id = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))

This definition is referenced by:  cidfval  17611  cidffn  17613