Definition df-cid 17570

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

This definition is referenced by:  cidfval  17577  cidffn  17579