# Metamath Proof Explorer

## Theorem rngosn4

Description: Obsolete as of 25-Jan-2020. Use rngen1zr instead. The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010) (Revised by Mario Carneiro, 30-Apr-2015) (New usage is discouraged.)

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

### Proof

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