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

Definition df-termo 17967
Description: An object A is called a terminal object provided that for each object B there is exactly one morphism from B to A. Definition 7.4 in [Adamek] p. 102, or definition in [Lang] p. 57 (called "a universally attracting object" there). See dftermo2 17986 and dftermo3 17988 for alternate definitions depending on df-inito 17966. (Contributed by AV, 3-Apr-2020.)
Assertion
Ref Expression
df-termo TermO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃! ∈ (𝑏(Hom ‘𝑐)𝑎)})
Distinct variable group:   𝑎,𝑏,𝑐,

Detailed syntax breakdown of Definition df-termo
StepHypRef Expression
1 ctermo 17964 . 2 class TermO
2 vc . . 3 setvar 𝑐
3 ccat 17637 . . 3 class Cat
4 vh . . . . . . . 8 setvar
54cv 1533 . . . . . . 7 class
6 vb . . . . . . . . 9 setvar 𝑏
76cv 1533 . . . . . . . 8 class 𝑏
8 va . . . . . . . . 9 setvar 𝑎
98cv 1533 . . . . . . . 8 class 𝑎
102cv 1533 . . . . . . . . 9 class 𝑐
11 chom 17237 . . . . . . . . 9 class Hom
1210, 11cfv 6542 . . . . . . . 8 class (Hom ‘𝑐)
137, 9, 12co 7414 . . . . . . 7 class (𝑏(Hom ‘𝑐)𝑎)
145, 13wcel 2099 . . . . . 6 wff ∈ (𝑏(Hom ‘𝑐)𝑎)
1514, 4weu 2558 . . . . 5 wff ∃! ∈ (𝑏(Hom ‘𝑐)𝑎)
16 cbs 17173 . . . . . 6 class Base
1710, 16cfv 6542 . . . . 5 class (Base‘𝑐)
1815, 6, 17wral 3057 . . . 4 wff 𝑏 ∈ (Base‘𝑐)∃! ∈ (𝑏(Hom ‘𝑐)𝑎)
1918, 8, 17crab 3428 . . 3 class {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃! ∈ (𝑏(Hom ‘𝑐)𝑎)}
202, 3, 19cmpt 5225 . 2 class (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃! ∈ (𝑏(Hom ‘𝑐)𝑎)})
211, 20wceq 1534 1 wff TermO = (𝑐 ∈ Cat ↦ {𝑎 ∈ (Base‘𝑐) ∣ ∀𝑏 ∈ (Base‘𝑐)∃! ∈ (𝑏(Hom ‘𝑐)𝑎)})
Colors of variables: wff setvar class
This definition is referenced by:  termofn  17970  termorcl  17973  termoval  17976  dftermo2  17986
  Copyright terms: Public domain W3C validator