Definition df-cid 16153

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 16149	. 2 class Id
2		vc	. . 3 setvar 𝑐
3		ccat 16148	. . 3 class Cat
4		vb	. . . 4 setvar 𝑏
5	2	cv 1474	. . . . 5 class 𝑐
6		cbs 15695	. . . . 5 class Base
7	5, 6	cfv 5804	. . . 4 class (Base‘𝑐)
8		vh	. . . . 5 setvar ℎ
9		chom 15779	. . . . . 6 class Hom
10	5, 9	cfv 5804	. . . . 5 class (Hom ‘𝑐)
11		vo	. . . . . 6 setvar 𝑜
12		cco 15780	. . . . . . 7 class comp
13	5, 12	cfv 5804	. . . . . 6 class (comp‘𝑐)
14		vx	. . . . . . 7 setvar 𝑥
15	4	cv 1474	. . . . . . 7 class 𝑏
16		vg	. . . . . . . . . . . . . 14 setvar 𝑔
17	16	cv 1474	. . . . . . . . . . . . 13 class 𝑔
18		vf	. . . . . . . . . . . . . 14 setvar 𝑓
19	18	cv 1474	. . . . . . . . . . . . 13 class 𝑓
20		vy	. . . . . . . . . . . . . . . 16 setvar 𝑦
21	20	cv 1474	. . . . . . . . . . . . . . 15 class 𝑦
22	14	cv 1474	. . . . . . . . . . . . . . 15 class 𝑥
23	21, 22	cop 4131	. . . . . . . . . . . . . 14 class ⟨𝑦, 𝑥⟩
24	11	cv 1474	. . . . . . . . . . . . . 14 class 𝑜
25	23, 22, 24	co 6549	. . . . . . . . . . . . 13 class (⟨𝑦, 𝑥⟩𝑜𝑥)
26	17, 19, 25	co 6549	. . . . . . . . . . . 12 class (𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓)
27	26, 19	wceq 1475	. . . . . . . . . . 11 wff (𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓
28	8	cv 1474	. . . . . . . . . . . 12 class ℎ
29	21, 22, 28	co 6549	. . . . . . . . . . 11 class (𝑦ℎ𝑥)
30	27, 18, 29	wral 2896	. . . . . . . . . 10 wff ∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓
31	22, 22	cop 4131	. . . . . . . . . . . . . 14 class ⟨𝑥, 𝑥⟩
32	31, 21, 24	co 6549	. . . . . . . . . . . . 13 class (⟨𝑥, 𝑥⟩𝑜𝑦)
33	19, 17, 32	co 6549	. . . . . . . . . . . 12 class (𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔)
34	33, 19	wceq 1475	. . . . . . . . . . 11 wff (𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓
35	22, 21, 28	co 6549	. . . . . . . . . . 11 class (𝑥ℎ𝑦)
36	34, 18, 35	wral 2896	. . . . . . . . . 10 wff ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓
37	30, 36	wa 383	. . . . . . . . 9 wff (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
38	37, 20, 15	wral 2896	. . . . . . . 8 wff ∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)
39	22, 22, 28	co 6549	. . . . . . . 8 class (𝑥ℎ𝑥)
40	38, 16, 39	crio 6510	. . . . . . 7 class (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))
41	14, 15, 40	cmpt 4643	. . . . . 6 class (𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
42	11, 13, 41	csb 3499	. . . . 5 class ⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
43	8, 10, 42	csb 3499	. . . 4 class ⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
44	4, 7, 43	csb 3499	. . 3 class ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓)))
45	2, 3, 44	cmpt 4643	. 2 class (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))
46	1, 45	wceq 1475	1 wff Id = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(⟨𝑦, 𝑥⟩𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(⟨𝑥, 𝑥⟩𝑜𝑦)𝑔) = 𝑓))))

This definition is referenced by:  cidfval  16160  cidffn  16162