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=BaseC
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=BaseC
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