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 16798
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 16794 . 2 class Id
2 vc . . 3 setvar 𝑐
3 ccat 16793 . . 3 class Cat
4 vb . . . 4 setvar 𝑏
52cv 1506 . . . . 5 class 𝑐
6 cbs 16339 . . . . 5 class Base
75, 6cfv 6188 . . . 4 class (Base‘𝑐)
8 vh . . . . 5 setvar
9 chom 16432 . . . . . 6 class Hom
105, 9cfv 6188 . . . . 5 class (Hom ‘𝑐)
11 vo . . . . . 6 setvar 𝑜
12 cco 16433 . . . . . . 7 class comp
135, 12cfv 6188 . . . . . 6 class (comp‘𝑐)
14 vx . . . . . . 7 setvar 𝑥
154cv 1506 . . . . . . 7 class 𝑏
16 vg . . . . . . . . . . . . . 14 setvar 𝑔
1716cv 1506 . . . . . . . . . . . . 13 class 𝑔
18 vf . . . . . . . . . . . . . 14 setvar 𝑓
1918cv 1506 . . . . . . . . . . . . 13 class 𝑓
20 vy . . . . . . . . . . . . . . . 16 setvar 𝑦
2120cv 1506 . . . . . . . . . . . . . . 15 class 𝑦
2214cv 1506 . . . . . . . . . . . . . . 15 class 𝑥
2321, 22cop 4447 . . . . . . . . . . . . . 14 class 𝑦, 𝑥
2411cv 1506 . . . . . . . . . . . . . 14 class 𝑜
2523, 22, 24co 6976 . . . . . . . . . . . . 13 class (⟨𝑦, 𝑥𝑜𝑥)
2617, 19, 25co 6976 . . . . . . . . . . . 12 class (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓)
2726, 19wceq 1507 . . . . . . . . . . 11 wff (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
288cv 1506 . . . . . . . . . . . 12 class
2921, 22, 28co 6976 . . . . . . . . . . 11 class (𝑦𝑥)
3027, 18, 29wral 3088 . . . . . . . . . 10 wff 𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓
3122, 22cop 4447 . . . . . . . . . . . . . 14 class 𝑥, 𝑥
3231, 21, 24co 6976 . . . . . . . . . . . . 13 class (⟨𝑥, 𝑥𝑜𝑦)
3319, 17, 32co 6976 . . . . . . . . . . . 12 class (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔)
3433, 19wceq 1507 . . . . . . . . . . 11 wff (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
3522, 21, 28co 6976 . . . . . . . . . . 11 class (𝑥𝑦)
3634, 18, 35wral 3088 . . . . . . . . . 10 wff 𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓
3730, 36wa 387 . . . . . . . . 9 wff (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
3837, 20, 15wral 3088 . . . . . . . 8 wff 𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)
3922, 22, 28co 6976 . . . . . . . 8 class (𝑥𝑥)
4038, 16, 39crio 6936 . . . . . . 7 class (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))
4114, 15, 40cmpt 5008 . . . . . 6 class (𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
4211, 13, 41csb 3786 . . . . 5 class (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
438, 10, 42csb 3786 . . . 4 class (Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
444, 7, 43csb 3786 . . 3 class (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓)))
452, 3, 44cmpt 5008 . 2 class (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))))
461, 45wceq 1507 1 wff Id = (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (comp‘𝑐) / 𝑜(𝑥𝑏 ↦ (𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓))))
Colors of variables: wff setvar class
This definition is referenced by:  cidfval  16805  cidffn  16807
  Copyright terms: Public domain W3C validator