Definition df-zeroo 16643

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 = ( c e. Cat |-> ( (InitO ` c ) i^i (TermO ` c ) ) )

Detailed syntax breakdown of Definition df-zeroo

Step	Hyp	Ref	Expression
1		czeroo 16640	. 2 class ZeroO
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4	2	cv 1482	. . . . 5 class c
5		cinito 16638	. . . . 5 class InitO
6	4, 5	cfv 5888	. . . 4 class (InitO ` c )
7		ctermo 16639	. . . . 5 class TermO
8	4, 7	cfv 5888	. . . 4 class (TermO ` c )
9	6, 8	cin 3573	. . 3 class ( (InitO ` c ) i^i (TermO ` c ) )
10	2, 3, 9	cmpt 4729	. 2 class ( c e. Cat |-> ( (InitO ` c ) i^i (TermO ` c ) ) )
11	1, 10	wceq 1483	1 wff ZeroO = ( c e. Cat |-> ( (InitO ` c ) i^i (TermO ` c ) ) )

This definition is referenced by:  zeroorcl  16646  zerooval  16649