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 17613
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 17609 . 2 class Id
2 vc . . 3 setvar 𝑐
3 ccat 17608 . . 3 class Cat
4 vb . . . 4 setvar 𝑏
52cv 1541 . . . . 5 class 𝑐
6 cbs 17144 . . . . 5 class Base
75, 6cfv 6544 . . . 4 class (Base‘𝑐)
8 vh . . . . 5 setvar
9 chom 17208 . . . . . 6 class Hom
105, 9cfv 6544 . . . . 5 class (Hom ‘𝑐)
11 vo . . . . . 6 setvar 𝑜
12 cco 17209 . . . . . . 7 class comp
135, 12cfv 6544 . . . . . 6 class (comp‘𝑐)
14 vx . . . . . . 7 setvar 𝑥
154cv 1541 . . . . . . 7 class 𝑏
16 vg . . . . . . . . . . . . . 14 setvar 𝑔
1716cv 1541 . . . . . . . . . . . . 13 class 𝑔
18 vf . . . . . . . . . . . . . 14 setvar 𝑓
1918cv 1541 . . . . . . . . . . . . 13 class 𝑓
20 vy . . . . . . . . . . . . . . . 16 setvar 𝑦
2120cv 1541 . . . . . . . . . . . . . . 15 class 𝑦
2214cv 1541 . . . . . . . . . . . . . . 15 class 𝑥
2321, 22cop 4635 . . . . . . . . . . . . . 14 class 𝑦, 𝑥
2411cv 1541 . . . . . . . . . . . . . 14 class 𝑜
2523, 22, 24co 7409 . . . . . . . . . . . . 13 class (⟨𝑦, 𝑥𝑜𝑥)
2617, 19, 25co 7409 . . . . . . . . . . . 12 class (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓)
2726, 19wceq 1542 . . . . . . . . . . 11 wff (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
288cv 1541 . . . . . . . . . . . 12 class
2921, 22, 28co 7409 . . . . . . . . . . 11 class (𝑦𝑥)
3027, 18, 29wral 3062 . . . . . . . . . 10 wff 𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
3122, 22cop 4635 . . . . . . . . . . . . . 14 class 𝑥, 𝑥
3231, 21, 24co 7409 . . . . . . . . . . . . 13 class (⟨𝑥, 𝑥𝑜𝑦)
3319, 17, 32co 7409 . . . . . . . . . . . 12 class (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔)
3433, 19wceq 1542 . . . . . . . . . . 11 wff (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
3522, 21, 28co 7409 . . . . . . . . . . 11 class (𝑥𝑦)
3634, 18, 35wral 3062 . . . . . . . . . 10 wff 𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
3730, 36wa 397 . . . . . . . . 9 wff (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
3837, 20, 15wral 3062 . . . . . . . 8 wff 𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
3922, 22, 28co 7409 . . . . . . . 8 class (𝑥𝑥)
4038, 16, 39crio 7364 . . . . . . 7 class (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))
4114, 15, 40cmpt 5232 . . . . . 6 class (𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
4211, 13, 41csb 3894 . . . . 5 class (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
438, 10, 42csb 3894 . . . 4 class (Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
444, 7, 43csb 3894 . . 3 class (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
452, 3, 44cmpt 5232 . 2 class (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))))
461, 45wceq 1542 1 wff Id = (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))))
Colors of variables: wff setvar class
This definition is referenced by:  cidfval  17620  cidffn  17622
  Copyright terms: Public domain W3C validator