Metamath Proof Explorer


Theorem iszeroi

Description: Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020)

Ref Expression
Assertion iszeroi
|- ( ( C e. Cat /\ O e. ( ZeroO ` C ) ) -> ( O e. ( Base ` C ) /\ ( O e. ( InitO ` C ) /\ O e. ( TermO ` C ) ) ) )

Proof

Step Hyp Ref Expression
1 id
 |-  ( C e. Cat -> C e. Cat )
2 eqid
 |-  ( Base ` C ) = ( Base ` C )
3 eqid
 |-  ( Hom ` C ) = ( Hom ` C )
4 1 2 3 zerooval
 |-  ( C e. Cat -> ( ZeroO ` C ) = ( ( InitO ` C ) i^i ( TermO ` C ) ) )
5 4 eleq2d
 |-  ( C e. Cat -> ( O e. ( ZeroO ` C ) <-> O e. ( ( InitO ` C ) i^i ( TermO ` C ) ) ) )
6 elin
 |-  ( O e. ( ( InitO ` C ) i^i ( TermO ` C ) ) <-> ( O e. ( InitO ` C ) /\ O e. ( TermO ` C ) ) )
7 initoo
 |-  ( C e. Cat -> ( O e. ( InitO ` C ) -> O e. ( Base ` C ) ) )
8 7 adantrd
 |-  ( C e. Cat -> ( ( O e. ( InitO ` C ) /\ O e. ( TermO ` C ) ) -> O e. ( Base ` C ) ) )
9 6 8 syl5bi
 |-  ( C e. Cat -> ( O e. ( ( InitO ` C ) i^i ( TermO ` C ) ) -> O e. ( Base ` C ) ) )
10 5 9 sylbid
 |-  ( C e. Cat -> ( O e. ( ZeroO ` C ) -> O e. ( Base ` C ) ) )
11 10 imp
 |-  ( ( C e. Cat /\ O e. ( ZeroO ` C ) ) -> O e. ( Base ` C ) )
12 simpl
 |-  ( ( C e. Cat /\ O e. ( Base ` C ) ) -> C e. Cat )
13 simpr
 |-  ( ( C e. Cat /\ O e. ( Base ` C ) ) -> O e. ( Base ` C ) )
14 2 3 12 13 iszeroo
 |-  ( ( C e. Cat /\ O e. ( Base ` C ) ) -> ( O e. ( ZeroO ` C ) <-> ( O e. ( InitO ` C ) /\ O e. ( TermO ` C ) ) ) )
15 14 biimpd
 |-  ( ( C e. Cat /\ O e. ( Base ` C ) ) -> ( O e. ( ZeroO ` C ) -> ( O e. ( InitO ` C ) /\ O e. ( TermO ` C ) ) ) )
16 15 impancom
 |-  ( ( C e. Cat /\ O e. ( ZeroO ` C ) ) -> ( O e. ( Base ` C ) -> ( O e. ( InitO ` C ) /\ O e. ( TermO ` C ) ) ) )
17 11 16 jcai
 |-  ( ( C e. Cat /\ O e. ( ZeroO ` C ) ) -> ( O e. ( Base ` C ) /\ ( O e. ( InitO ` C ) /\ O e. ( TermO ` C ) ) ) )