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

Definition df-zeroo 17711
Description: An object A is called a zero object provided that it is both an initial object and a terminal object. Definition 7.7 of [Adamek] p. 103. (Contributed by AV, 3-Apr-2020.)
Assertion
Ref Expression
df-zeroo ZeroO = (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐)))

Detailed syntax breakdown of Definition df-zeroo
StepHypRef Expression
1 czeroo 17708 . 2 class ZeroO
2 vc . . 3 setvar 𝑐
3 ccat 17383 . . 3 class Cat
42cv 1538 . . . . 5 class 𝑐
5 cinito 17706 . . . . 5 class InitO
64, 5cfv 6426 . . . 4 class (InitO‘𝑐)
7 ctermo 17707 . . . . 5 class TermO
84, 7cfv 6426 . . . 4 class (TermO‘𝑐)
96, 8cin 3885 . . 3 class ((InitO‘𝑐) ∩ (TermO‘𝑐))
102, 3, 9cmpt 5156 . 2 class (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐)))
111, 10wceq 1539 1 wff ZeroO = (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐)))
Colors of variables: wff setvar class
This definition is referenced by:  zeroofn  17714  zeroorcl  17717  zerooval  17720
  Copyright terms: Public domain W3C validator