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 = ( 𝑐 ∈ 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 ‘ 𝑐 ) ) )