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 = ( 1st ` R )
	on1el3.2	|- X = ran G
Assertion	rngosn4	|- ( ( R e. RingOps /\ A e. X ) -> ( X ~~ 1o <-> R = <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. ) )

Proof

Step	Hyp	Ref	Expression
1		on1el3.1	|- G = ( 1st ` R )
2		on1el3.2	|- X = ran G
3		en1eqsnbi	|- ( A e. X -> ( X ~~ 1o <-> X = { A } ) )
4	3	adantl	|- ( ( R e. RingOps /\ A e. X ) -> ( X ~~ 1o <-> X = { A } ) )
5	1 2	rngosn3	|- ( ( R e. RingOps /\ A e. X ) -> ( X = { A } <-> R = <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. ) )
6	4 5	bitrd	|- ( ( R e. RingOps /\ A e. X ) -> ( X ~~ 1o <-> R = <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. ) )