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	|- ( ph -> U e. V )
	zrinitorngc.c	|- C = ( RngCat ` U )
	zrinitorngc.z	|- ( ph -> Z e. ( Ring \ NzRing ) )
	zrinitorngc.e	|- ( ph -> Z e. U )
Assertion	zrzeroorngc	|- ( ph -> Z e. ( ZeroO ` C ) )

Proof

Step	Hyp	Ref	Expression
1		zrinitorngc.u	|- ( ph -> U e. V )
2		zrinitorngc.c	|- C = ( RngCat ` U )
3		zrinitorngc.z	|- ( ph -> Z e. ( Ring \ NzRing ) )
4		zrinitorngc.e	|- ( ph -> Z e. U )
5	1 2 3 4	zrinitorngc	|- ( ph -> Z e. ( InitO ` C ) )
6	1 2 3 4	zrtermorngc	|- ( ph -> Z e. ( TermO ` C ) )
7		eqid	|- ( Base ` C ) = ( Base ` C )
8		eqid	|- ( Hom ` C ) = ( Hom ` C )
9	2	rngccat	|- ( U e. V -> C e. Cat )
10	1 9	syl	|- ( ph -> C e. Cat )
11	3	eldifad	|- ( ph -> Z e. Ring )
12		ringrng	|- ( Z e. Ring -> Z e. Rng )
13	11 12	syl	|- ( ph -> Z e. Rng )
14	4 13	elind	|- ( ph -> Z e. ( U i^i Rng ) )
15	2 7 1	rngcbas	|- ( ph -> ( Base ` C ) = ( U i^i Rng ) )
16	14 15	eleqtrrd	|- ( ph -> Z e. ( Base ` C ) )
17	7 8 10 16	iszeroo	|- ( ph -> ( Z e. ( ZeroO ` C ) <-> ( Z e. ( InitO ` C ) /\ Z e. ( TermO ` C ) ) ) )
18	5 6 17	mpbir2and	|- ( ph -> Z e. ( ZeroO ` C ) )