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 17253
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 17250 . 2 class ZeroO
2 vc . . 3 setvar 𝑐
3 ccat 16935 . . 3 class Cat
42cv 1537 . . . . 5 class 𝑐
5 cinito 17248 . . . . 5 class InitO
64, 5cfv 6343 . . . 4 class (InitO‘𝑐)
7 ctermo 17249 . . . . 5 class TermO
84, 7cfv 6343 . . . 4 class (TermO‘𝑐)
96, 8cin 3918 . . 3 class ((InitO‘𝑐) ∩ (TermO‘𝑐))
102, 3, 9cmpt 5132 . 2 class (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐)))
111, 10wceq 1538 1 wff ZeroO = (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐)))
Colors of variables: wff setvar class
This definition is referenced by:  zeroorcl  17256  zerooval  17259
  Copyright terms: Public domain W3C validator