MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cid Structured version   Visualization version   GIF version

Definition df-cid 17713
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
StepHypRef Expression
1 ccid 17709 . 2 class Id
2 vc . . 3 setvar 𝑐
3 ccat 17708 . . 3 class Cat
4 vb . . . 4 setvar 𝑏
52cv 1535 . . . . 5 class 𝑐
6 cbs 17244 . . . . 5 class Base
75, 6cfv 6562 . . . 4 class (Base‘𝑐)
8 vh . . . . 5 setvar
9 chom 17308 . . . . . 6 class Hom
105, 9cfv 6562 . . . . 5 class (Hom ‘𝑐)
11 vo . . . . . 6 setvar 𝑜
12 cco 17309 . . . . . . 7 class comp
135, 12cfv 6562 . . . . . 6 class (comp‘𝑐)
14 vx . . . . . . 7 setvar 𝑥
154cv 1535 . . . . . . 7 class 𝑏
16 vg . . . . . . . . . . . . . 14 setvar 𝑔
1716cv 1535 . . . . . . . . . . . . 13 class 𝑔
18 vf . . . . . . . . . . . . . 14 setvar 𝑓
1918cv 1535 . . . . . . . . . . . . 13 class 𝑓
20 vy . . . . . . . . . . . . . . . 16 setvar 𝑦
2120cv 1535 . . . . . . . . . . . . . . 15 class 𝑦
2214cv 1535 . . . . . . . . . . . . . . 15 class 𝑥
2321, 22cop 4636 . . . . . . . . . . . . . 14 class 𝑦, 𝑥
2411cv 1535 . . . . . . . . . . . . . 14 class 𝑜
2523, 22, 24co 7430 . . . . . . . . . . . . 13 class (⟨𝑦, 𝑥𝑜𝑥)
2617, 19, 25co 7430 . . . . . . . . . . . 12 class (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓)
2726, 19wceq 1536 . . . . . . . . . . 11 wff (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
288cv 1535 . . . . . . . . . . . 12 class
2921, 22, 28co 7430 . . . . . . . . . . 11 class (𝑦𝑥)
3027, 18, 29wral 3058 . . . . . . . . . 10 wff 𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
3122, 22cop 4636 . . . . . . . . . . . . . 14 class 𝑥, 𝑥
3231, 21, 24co 7430 . . . . . . . . . . . . 13 class (⟨𝑥, 𝑥𝑜𝑦)
3319, 17, 32co 7430 . . . . . . . . . . . 12 class (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔)
3433, 19wceq 1536 . . . . . . . . . . 11 wff (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
3522, 21, 28co 7430 . . . . . . . . . . 11 class (𝑥𝑦)
3634, 18, 35wral 3058 . . . . . . . . . 10 wff 𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
3730, 36wa 395 . . . . . . . . 9 wff (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
3837, 20, 15wral 3058 . . . . . . . 8 wff 𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
3922, 22, 28co 7430 . . . . . . . 8 class (𝑥𝑥)
4038, 16, 39crio 7386 . . . . . . 7 class (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))
4114, 15, 40cmpt 5230 . . . . . 6 class (𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
4211, 13, 41csb 3907 . . . . 5 class (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
438, 10, 42csb 3907 . . . 4 class (Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
444, 7, 43csb 3907 . . 3 class (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
452, 3, 44cmpt 5230 . 2 class (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))))
461, 45wceq 1536 1 wff Id = (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))))
Colors of variables: wff setvar class
This definition is referenced by:  cidfval  17720  cidffn  17722
  Copyright terms: Public domain W3C validator