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 ∈ Base C ∧ O ∈ InitO ⁡ C ∧ O ∈ TermO ⁡ C

Proof

Step Hyp Ref Expression
1 id ⊢ C ∈ Cat → C ∈ Cat
2 eqid ⊢ Base C = Base C
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 ∈ Base C
8 7 adantrd ⊢ C ∈ Cat → O ∈ InitO ⁡ C ∧ O ∈ TermO ⁡ C → O ∈ Base C
9 6 8 syl5bi ⊢ C ∈ Cat → O ∈ InitO ⁡ C ∩ TermO ⁡ C → O ∈ Base C
10 5 9 sylbid ⊢ C ∈ Cat → O ∈ ZeroO ⁡ C → O ∈ Base C
11 10 imp ⊢ C ∈ Cat ∧ O ∈ ZeroO ⁡ C → O ∈ Base C
12 simpl ⊢ C ∈ Cat ∧ O ∈ Base C → C ∈ Cat
13 simpr ⊢ C ∈ Cat ∧ O ∈ Base C → O ∈ Base C
14 2 3 12 13 iszeroo ⊢ C ∈ Cat ∧ O ∈ Base C → O ∈ ZeroO ⁡ C ↔ O ∈ InitO ⁡ C ∧ O ∈ TermO ⁡ C
15 14 biimpd ⊢ C ∈ Cat ∧ O ∈ Base C → O ∈ ZeroO ⁡ C → O ∈ InitO ⁡ C ∧ O ∈ TermO ⁡ C
16 15 impancom ⊢ C ∈ Cat ∧ O ∈ ZeroO ⁡ C → O ∈ Base C → O ∈ InitO ⁡ C ∧ O ∈ TermO ⁡ C
17 11 16 jcai ⊢ C ∈ Cat ∧ O ∈ ZeroO ⁡ C → O ∈ Base C ∧ O ∈ InitO ⁡ C ∧ O ∈ TermO ⁡ C