Metamath Proof Explorer

Definition df-zeroo

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)

		Ref	Expression
	Assertion	df-zeroo	$⊢ ZeroO = (c \in Cat ⟼ InitO (c) \cap TermO (c))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czeroo	$class ZeroO$
1		vc	$setvar c$
2		ccat	$class Cat$
3		cinito	$class InitO$
4	1	cv	$setvar c$
5	4 3	cfv	$class InitO (c)$
6		ctermo	$class TermO$
7	4 6	cfv	$class TermO (c)$
8	5 7	cin	$class (InitO (c) \cap TermO (c))$
9	1 2 8	cmpt	$class (c \in Cat ⟼ InitO (c) \cap TermO (c))$
10	0 9	wceq	$wff ZeroO = (c \in Cat ⟼ InitO (c) \cap TermO (c))$