Definition df-zeroo 18081

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

Step	Hyp	Ref	Expression
1		czeroo 18078	. 2 class ZeroO
2		vc	. . 3 setvar 𝑐
3		ccat 17758	. . 3 class Cat
4	2	cv 1569	. . . . 5 class 𝑐
5		cinito 18076	. . . . 5 class InitO
6	4, 5	cfv 6537	. . . 4 class (InitO‘𝑐)
7		ctermo 18077	. . . . 5 class TermO
8	4, 7	cfv 6537	. . . 4 class (TermO‘𝑐)
9	6, 8	cin 3901	. . 3 class ((InitO‘𝑐) ∩ (TermO‘𝑐))
10	2, 3, 9	cmpt 5190	. 2 class (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐)))
11	1, 10	wceq 1570	1 wff ZeroO = (𝑐 ∈ Cat ↦ ((InitO‘𝑐) ∩ (TermO‘𝑐)))

This definition is used by:  zeroofn  18084  zeroorcl  18087  zerooval  18090