# 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 ${⊢}\mathrm{ZeroO}=\left({c}\in \mathrm{Cat}⟼\mathrm{InitO}\left({c}\right)\cap \mathrm{TermO}\left({c}\right)\right)$

### Detailed syntax breakdown

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