Theorem zrzeroorngc

Description: The zero ring is a zero object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020)

	Ref	Expression
Hypotheses	zrinitorngc.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	zrinitorngc.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
	zrinitorngc.z	⊢ ( 𝜑 → 𝑍 ∈ ( Ring ∖ NzRing ) )
	zrinitorngc.e	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
Assertion	zrzeroorngc	⊢ ( 𝜑 → 𝑍 ∈ ( ZeroO ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		zrinitorngc.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2		zrinitorngc.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
3		zrinitorngc.z	⊢ ( 𝜑 → 𝑍 ∈ ( Ring ∖ NzRing ) )
4		zrinitorngc.e	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
5	1 2 3 4	zrinitorngc	⊢ ( 𝜑 → 𝑍 ∈ ( InitO ‘ 𝐶 ) )
6	1 2 3 4	zrtermorngc	⊢ ( 𝜑 → 𝑍 ∈ ( TermO ‘ 𝐶 ) )
7		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9	2	rngccat	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
10	1 9	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
11	3	eldifad	⊢ ( 𝜑 → 𝑍 ∈ Ring )
12		ringrng	⊢ ( 𝑍 ∈ Ring → 𝑍 ∈ Rng )
13	11 12	syl	⊢ ( 𝜑 → 𝑍 ∈ Rng )
14	4 13	elind	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑈 ∩ Rng ) )
15	2 7 1	rngcbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Rng ) )
16	14 15	eleqtrrd	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
17	7 8 10 16	iszeroo	⊢ ( 𝜑 → ( 𝑍 ∈ ( ZeroO ‘ 𝐶 ) ↔ ( 𝑍 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑍 ∈ ( TermO ‘ 𝐶 ) ) ) )
18	5 6 17	mpbir2and	⊢ ( 𝜑 → 𝑍 ∈ ( ZeroO ‘ 𝐶 ) )