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 ) ) ) ) |
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 ) ) ) ) |