Metamath Proof Explorer


Theorem iszeroo

Description: The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020)

Ref Expression
Hypotheses isinito.b B = Base C
isinito.h H = Hom C
isinito.c φ C Cat
isinito.i φ I B
Assertion iszeroo φ I ZeroO C I InitO C I TermO C

Proof

Step Hyp Ref Expression
1 isinito.b B = Base C
2 isinito.h H = Hom C
3 isinito.c φ C Cat
4 isinito.i φ I B
5 3 1 2 zerooval φ ZeroO C = InitO C TermO C
6 5 eleq2d φ I ZeroO C I InitO C TermO C
7 elin I InitO C TermO C I InitO C I TermO C
8 6 7 bitrdi φ I ZeroO C I InitO C I TermO C