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∈Cat∧O∈ZeroO⁡C→O∈BaseC∧O∈InitO⁡C∧O∈TermO⁡C

Proof

Step Hyp Ref Expression
1 id ⊢C∈Cat→C∈Cat
2 eqid ⊢BaseC=BaseC
3 eqid ⊢Hom⁡C=Hom⁡C
4 1 2 3 zerooval ⊢C∈Cat→ZeroO⁡C=InitO⁡C∩TermO⁡C
5 4 eleq2d ⊢C∈Cat→O∈ZeroO⁡C↔O∈InitO⁡C∩TermO⁡C
6 elin ⊢O∈InitO⁡C∩TermO⁡C↔O∈InitO⁡C∧O∈TermO⁡C
7 initoo ⊢C∈Cat→O∈InitO⁡C→O∈BaseC
8 7 adantrd ⊢C∈Cat→O∈InitO⁡C∧O∈TermO⁡C→O∈BaseC
9 6 8 biimtrid ⊢C∈Cat→O∈InitO⁡C∩TermO⁡C→O∈BaseC
10 5 9 sylbid ⊢C∈Cat→O∈ZeroO⁡C→O∈BaseC
11 10 imp ⊢C∈Cat∧O∈ZeroO⁡C→O∈BaseC
12 simpl ⊢C∈Cat∧O∈BaseC→C∈Cat
13 simpr ⊢C∈Cat∧O∈BaseC→O∈BaseC
14 2 3 12 13 iszeroo ⊢C∈Cat∧O∈BaseC→O∈ZeroO⁡C↔O∈InitO⁡C∧O∈TermO⁡C
15 14 biimpd ⊢C∈Cat∧O∈BaseC→O∈ZeroO⁡C→O∈InitO⁡C∧O∈TermO⁡C
16 15 impancom ⊢C∈Cat∧O∈ZeroO⁡C→O∈BaseC→O∈InitO⁡C∧O∈TermO⁡C
17 11 16 jcai ⊢C∈Cat∧O∈ZeroO⁡C→O∈BaseC∧O∈InitO⁡C∧O∈TermO⁡C