Metamath Proof Explorer


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

Proof

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