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 𝐵 = ( 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 ‘ 𝐶 ) ) ) )