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 16412
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 16409 . 2 class ZeroO
2 vc . . 3 setvar 𝑐
3 ccat 16094 . . 3 class Cat
42cv 1473 . . . . 5 class 𝑐
5 cinito 16407 . . . . 5 class InitO
64, 5cfv 5790 . . . 4 class (InitO‘𝑐)
7 ctermo 16408 . . . . 5 class TermO
84, 7cfv 5790 . . . 4 class (TermO‘𝑐)
96, 8cin 3538 . . 3 class ((InitO‘𝑐) ∩ (TermO‘𝑐))
102, 3, 9cmpt 4637 . 2 class (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐)))
111, 10wceq 1474 1 wff ZeroO = (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐)))
Colors of variables: wff setvar class
This definition is referenced by:  zeroorcl  16415  zerooval  16418
  Copyright terms: Public domain W3C validator