Theorem iszeroo

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

	Ref	Expression
Hypotheses	isinito.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	isinito.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	isinito.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	isinito.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
Assertion	iszeroo	⊢ ( 𝜑 → ( 𝐼 ∈ ( ZeroO ‘ 𝐶 ) ↔ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ∧ 𝐼 ∈ ( TermO ‘ 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isinito.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		isinito.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		isinito.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		isinito.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
5	3 1 2	zerooval	⊢ ( 𝜑 → ( ZeroO ‘ 𝐶 ) = ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) )
6	5	eleq2d	⊢ ( 𝜑 → ( 𝐼 ∈ ( ZeroO ‘ 𝐶 ) ↔ 𝐼 ∈ ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) ) )
7		elin	⊢ ( 𝐼 ∈ ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) ↔ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ∧ 𝐼 ∈ ( TermO ‘ 𝐶 ) ) )
8	6 7	bitrdi	⊢ ( 𝜑 → ( 𝐼 ∈ ( ZeroO ‘ 𝐶 ) ↔ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ∧ 𝐼 ∈ ( TermO ‘ 𝐶 ) ) ) )