Database
BASIC CATEGORY THEORY
Categories
Initial, terminal and zero objects of a category
df-zeroo
Metamath Proof Explorer
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 ‘ 𝑐 ) ) )