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