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