This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iszeroi

Description: Implication of a class being a zero object. (Contributed by AV, 18-Apr-2020)

Ref Expression
Assertion iszeroi ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( ZeroO ‘ 𝐶 ) ) → ( 𝑂 ∈ ( Base ‘ 𝐶 ) ∧ ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑂 ∈ ( TermO ‘ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat )
2 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
3 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
4 1 2 3 zerooval ⊢ ( 𝐶 ∈ Cat → ( ZeroO ‘ 𝐶 ) = ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) )
5 4 eleq2d ⊢ ( 𝐶 ∈ Cat → ( 𝑂 ∈ ( ZeroO ‘ 𝐶 ) ↔ 𝑂 ∈ ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) ) )
6 elin ⊢ ( 𝑂 ∈ ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) ↔ ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑂 ∈ ( TermO ‘ 𝐶 ) ) )
7 initoo ⊢ ( 𝐶 ∈ Cat → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → 𝑂 ∈ ( Base ‘ 𝐶 ) ) )
8 7 adantrd ⊢ ( 𝐶 ∈ Cat → ( ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑂 ∈ ( TermO ‘ 𝐶 ) ) → 𝑂 ∈ ( Base ‘ 𝐶 ) ) )
9 6 8 biimtrid ⊢ ( 𝐶 ∈ Cat → ( 𝑂 ∈ ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) → 𝑂 ∈ ( Base ‘ 𝐶 ) ) )
10 5 9 sylbid ⊢ ( 𝐶 ∈ Cat → ( 𝑂 ∈ ( ZeroO ‘ 𝐶 ) → 𝑂 ∈ ( Base ‘ 𝐶 ) ) )
11 10 imp ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( ZeroO ‘ 𝐶 ) ) → 𝑂 ∈ ( Base ‘ 𝐶 ) )
12 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
13 simpr ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( Base ‘ 𝐶 ) ) → 𝑂 ∈ ( Base ‘ 𝐶 ) )
14 2 3 12 13 iszeroo ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑂 ∈ ( ZeroO ‘ 𝐶 ) ↔ ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑂 ∈ ( TermO ‘ 𝐶 ) ) ) )
15 14 biimpd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑂 ∈ ( ZeroO ‘ 𝐶 ) → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑂 ∈ ( TermO ‘ 𝐶 ) ) ) )
16 15 impancom ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( ZeroO ‘ 𝐶 ) ) → ( 𝑂 ∈ ( Base ‘ 𝐶 ) → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑂 ∈ ( TermO ‘ 𝐶 ) ) ) )
17 11 16 jcai ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( ZeroO ‘ 𝐶 ) ) → ( 𝑂 ∈ ( Base ‘ 𝐶 ) ∧ ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑂 ∈ ( TermO ‘ 𝐶 ) ) ) )