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 16251
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 16247 . 2 class Id
2 vc . . 3 setvar 𝑐
3 ccat 16246 . . 3 class Cat
4 vb . . . 4 setvar 𝑏
52cv 1479 . . . . 5 class 𝑐
6 cbs 15781 . . . . 5 class Base
75, 6cfv 5847 . . . 4 class (Base‘𝑐)
8 vh . . . . 5 setvar
9 chom 15873 . . . . . 6 class Hom
105, 9cfv 5847 . . . . 5 class (Hom ‘𝑐)
11 vo . . . . . 6 setvar 𝑜
12 cco 15874 . . . . . . 7 class comp
135, 12cfv 5847 . . . . . 6 class (comp‘𝑐)
14 vx . . . . . . 7 setvar 𝑥
154cv 1479 . . . . . . 7 class 𝑏
16 vg . . . . . . . . . . . . . 14 setvar 𝑔
1716cv 1479 . . . . . . . . . . . . 13 class 𝑔
18 vf . . . . . . . . . . . . . 14 setvar 𝑓
1918cv 1479 . . . . . . . . . . . . 13 class 𝑓
20 vy . . . . . . . . . . . . . . . 16 setvar 𝑦
2120cv 1479 . . . . . . . . . . . . . . 15 class 𝑦
2214cv 1479 . . . . . . . . . . . . . . 15 class 𝑥
2321, 22cop 4154 . . . . . . . . . . . . . 14 class 𝑦, 𝑥
2411cv 1479 . . . . . . . . . . . . . 14 class 𝑜
2523, 22, 24co 6604 . . . . . . . . . . . . 13 class (⟨𝑦, 𝑥𝑜𝑥)
2617, 19, 25co 6604 . . . . . . . . . . . 12 class (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓)
2726, 19wceq 1480 . . . . . . . . . . 11 wff (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
288cv 1479 . . . . . . . . . . . 12 class
2921, 22, 28co 6604 . . . . . . . . . . 11 class (𝑦𝑥)
3027, 18, 29wral 2907 . . . . . . . . . 10 wff 𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
3122, 22cop 4154 . . . . . . . . . . . . . 14 class 𝑥, 𝑥
3231, 21, 24co 6604 . . . . . . . . . . . . 13 class (⟨𝑥, 𝑥𝑜𝑦)
3319, 17, 32co 6604 . . . . . . . . . . . 12 class (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔)
3433, 19wceq 1480 . . . . . . . . . . 11 wff (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
3522, 21, 28co 6604 . . . . . . . . . . 11 class (𝑥𝑦)
3634, 18, 35wral 2907 . . . . . . . . . 10 wff 𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
3730, 36wa 384 . . . . . . . . 9 wff (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
3837, 20, 15wral 2907 . . . . . . . 8 wff 𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
3922, 22, 28co 6604 . . . . . . . 8 class (𝑥𝑥)
4038, 16, 39crio 6564 . . . . . . 7 class (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))
4114, 15, 40cmpt 4673 . . . . . 6 class (𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
4211, 13, 41csb 3514 . . . . 5 class (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
438, 10, 42csb 3514 . . . 4 class (Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
444, 7, 43csb 3514 . . 3 class (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
452, 3, 44cmpt 4673 . 2 class (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))))
461, 45wceq 1480 1 wff Id = (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))))
Colors of variables: wff setvar class
This definition is referenced by:  cidfval  16258  cidffn  16260
  Copyright terms: Public domain W3C validator