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 ‘ 𝐶 ) ) ) )