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
|- ( ph -> C e. Cat )
isinito.i
|- ( ph -> I e. B )
Assertion iszeroo
|- ( ph -> ( I e. ( ZeroO ` C ) <-> ( I e. ( InitO ` C ) /\ I e. ( TermO ` C ) ) ) )

Proof

Step Hyp Ref Expression
1 isinito.b
 |-  B = ( Base ` C )
2 isinito.h
 |-  H = ( Hom ` C )
3 isinito.c
 |-  ( ph -> C e. Cat )
4 isinito.i
 |-  ( ph -> I e. B )
5 3 1 2 zerooval
 |-  ( ph -> ( ZeroO ` C ) = ( ( InitO ` C ) i^i ( TermO ` C ) ) )
6 5 eleq2d
 |-  ( ph -> ( I e. ( ZeroO ` C ) <-> I e. ( ( InitO ` C ) i^i ( TermO ` C ) ) ) )
7 elin
 |-  ( I e. ( ( InitO ` C ) i^i ( TermO ` C ) ) <-> ( I e. ( InitO ` C ) /\ I e. ( TermO ` C ) ) )
8 6 7 bitrdi
 |-  ( ph -> ( I e. ( ZeroO ` C ) <-> ( I e. ( InitO ` C ) /\ I e. ( TermO ` C ) ) ) )