Metamath Proof Explorer

Theorem iszeroo

Description: The predicate "is a zero object" of a category. (Contributed by AV, 3-Apr-2020)

Ref Expression
Hypotheses isinito.b ⊢ B = Base C
isinito.h ⊢ H = Hom ⁡ C
isinito.c ⊢ φ → C ∈ Cat
isinito.i ⊢ φ → I ∈ B
Assertion iszeroo ⊢ φ → I ∈ ZeroO ⁡ C ↔ I ∈ InitO ⁡ C ∧ I ∈ TermO ⁡ C

Proof

Step Hyp Ref Expression
1 isinito.b ⊢ B = Base C
2 isinito.h ⊢ H = Hom ⁡ C
3 isinito.c ⊢ φ → C ∈ Cat
4 isinito.i ⊢ φ → I ∈ B
5 3 1 2 zerooval ⊢ φ → ZeroO ⁡ C = InitO ⁡ C ∩ TermO ⁡ C
6 5 eleq2d ⊢ φ → I ∈ ZeroO ⁡ C ↔ I ∈ InitO ⁡ C ∩ TermO ⁡ C
7 elin ⊢ I ∈ InitO ⁡ C ∩ TermO ⁡ C ↔ I ∈ InitO ⁡ C ∧ I ∈ TermO ⁡ C
8 6 7 bitrdi ⊢ φ → I ∈ ZeroO ⁡ C ↔ I ∈ InitO ⁡ C ∧ I ∈ TermO ⁡ C