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 = ( 𝑐 ∈ Cat ↦ ( ( InitO ‘ 𝑐 ) ∩ ( TermO ‘ 𝑐 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czeroo	⊢ ZeroO
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		cinito	⊢ InitO
4	1	cv	⊢ 𝑐
5	4 3	cfv	⊢ ( InitO ‘ 𝑐 )
6		ctermo	⊢ TermO
7	4 6	cfv	⊢ ( TermO ‘ 𝑐 )
8	5 7	cin	⊢ ( ( InitO ‘ 𝑐 ) ∩ ( TermO ‘ 𝑐 ) )
9	1 2 8	cmpt	⊢ ( 𝑐 ∈ Cat ↦ ( ( InitO ‘ 𝑐 ) ∩ ( TermO ‘ 𝑐 ) ) )
10	0 9	wceq	⊢ ZeroO = ( 𝑐 ∈ Cat ↦ ( ( InitO ‘ 𝑐 ) ∩ ( TermO ‘ 𝑐 ) ) )