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

Definition df-inito 16842
 Description: An object A is said to be an initial object provided that for each object B there is exactly one morphism from A to B. Definition 7.1 in [Adamek] p. 101, or definition in [Lang] p. 57 (called "a universally repelling object" there). (Contributed by AV, 3-Apr-2020.)
Assertion
Ref Expression
df-inito InitO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃! ∈ (𝑎(Hom ‘𝑐)𝑏)})
Distinct variable group:   𝑎,𝑏,𝑐,

Detailed syntax breakdown of Definition df-inito
StepHypRef Expression
1 cinito 16839 . 2 class InitO
2 vc . . 3 setvar 𝑐
3 ccat 16526 . . 3 class Cat
4 vh . . . . . . . 8 setvar
54cv 1631 . . . . . . 7 class
6 va . . . . . . . . 9 setvar 𝑎
76cv 1631 . . . . . . . 8 class 𝑎
8 vb . . . . . . . . 9 setvar 𝑏
98cv 1631 . . . . . . . 8 class 𝑏
102cv 1631 . . . . . . . . 9 class 𝑐
11 chom 16154 . . . . . . . . 9 class Hom
1210, 11cfv 6049 . . . . . . . 8 class (Hom ‘𝑐)
137, 9, 12co 6813 . . . . . . 7 class (𝑎(Hom ‘𝑐)𝑏)
145, 13wcel 2139 . . . . . 6 wff ∈ (𝑎(Hom ‘𝑐)𝑏)
1514, 4weu 2607 . . . . 5 wff ∃! ∈ (𝑎(Hom ‘𝑐)𝑏)
16 cbs 16059 . . . . . 6 class Base
1710, 16cfv 6049 . . . . 5 class (Base‘𝑐)
1815, 8, 17wral 3050 . . . 4 wff 𝑏 ∈ (Base‘𝑐)∃! ∈ (𝑎(Hom ‘𝑐)𝑏)
1918, 6, 17crab 3054 . . 3 class {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃! ∈ (𝑎(Hom ‘𝑐)𝑏)}
202, 3, 19cmpt 4881 . 2 class (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃! ∈ (𝑎(Hom ‘𝑐)𝑏)})
211, 20wceq 1632 1 wff InitO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃! ∈ (𝑎(Hom ‘𝑐)𝑏)})
 Colors of variables: wff setvar class This definition is referenced by:  initorcl  16845  initoval  16848
 Copyright terms: Public domain W3C validator