This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC CATEGORY THEORY Categories Initial, terminal and zero objects of a category 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 ‘ 𝑐 ) ) )