# Metamath Proof Explorer

## Theorem rngosn6

Description: Obsolete as of 25-Jan-2020. Use ringen1zr or srgen1zr instead. The only unital ring with one element is the zero ring. (Contributed by FL, 15-Feb-2010) (New usage is discouraged.)

Ref Expression
Hypotheses on1el3.1 ${⊢}{G}={1}^{st}\left({R}\right)$
on1el3.2 ${⊢}{X}=\mathrm{ran}{G}$
on1el3.3 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
Assertion rngosn6 ${⊢}{R}\in \mathrm{RingOps}\to \left({X}\approx {1}_{𝑜}↔{R}=⟨\left\{⟨⟨{Z},{Z}⟩,{Z}⟩\right\},\left\{⟨⟨{Z},{Z}⟩,{Z}⟩\right\}⟩\right)$

### Proof

Step Hyp Ref Expression
1 on1el3.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 on1el3.2 ${⊢}{X}=\mathrm{ran}{G}$
3 on1el3.3 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
4 1 2 3 rngo0cl ${⊢}{R}\in \mathrm{RingOps}\to {Z}\in {X}$
5 1 2 rngosn4 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {Z}\in {X}\right)\to \left({X}\approx {1}_{𝑜}↔{R}=⟨\left\{⟨⟨{Z},{Z}⟩,{Z}⟩\right\},\left\{⟨⟨{Z},{Z}⟩,{Z}⟩\right\}⟩\right)$
6 4 5 mpdan ${⊢}{R}\in \mathrm{RingOps}\to \left({X}\approx {1}_{𝑜}↔{R}=⟨\left\{⟨⟨{Z},{Z}⟩,{Z}⟩\right\},\left\{⟨⟨{Z},{Z}⟩,{Z}⟩\right\}⟩\right)$