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

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