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