Theorem rngo1cl

Description: The unity element of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ring1cl.1	|- X = ran ( 1st ` R )
	ring1cl.2	|- H = ( 2nd ` R )
	ring1cl.3	|- U = ( GId ` H )
Assertion	rngo1cl	|- ( R e. RingOps -> U e. X )

Proof

Step	Hyp	Ref	Expression
1		ring1cl.1	|- X = ran ( 1st ` R )
2		ring1cl.2	|- H = ( 2nd ` R )
3		ring1cl.3	|- U = ( GId ` H )
4	2	rngomndo	|- ( R e. RingOps -> H e. MndOp )
5	2	eleq1i	|- ( H e. MndOp <-> ( 2nd ` R ) e. MndOp )
6		mndoismgmOLD	|- ( ( 2nd ` R ) e. MndOp -> ( 2nd ` R ) e. Magma )
7		mndoisexid	|- ( ( 2nd ` R ) e. MndOp -> ( 2nd ` R ) e. ExId )
8	6 7	jca	|- ( ( 2nd ` R ) e. MndOp -> ( ( 2nd ` R ) e. Magma /\ ( 2nd ` R ) e. ExId ) )
9	5 8	sylbi	|- ( H e. MndOp -> ( ( 2nd ` R ) e. Magma /\ ( 2nd ` R ) e. ExId ) )
10	4 9	syl	|- ( R e. RingOps -> ( ( 2nd ` R ) e. Magma /\ ( 2nd ` R ) e. ExId ) )
11		elin	|- ( ( 2nd ` R ) e. ( Magma i^i ExId ) <-> ( ( 2nd ` R ) e. Magma /\ ( 2nd ` R ) e. ExId ) )
12	10 11	sylibr	|- ( R e. RingOps -> ( 2nd ` R ) e. ( Magma i^i ExId ) )
13		eqid	|- ran ( 2nd ` R ) = ran ( 2nd ` R )
14	2	fveq2i	|- ( GId ` H ) = ( GId ` ( 2nd ` R ) )
15	3 14	eqtri	|- U = ( GId ` ( 2nd ` R ) )
16	13 15	iorlid	|- ( ( 2nd ` R ) e. ( Magma i^i ExId ) -> U e. ran ( 2nd ` R ) )
17	12 16	syl	|- ( R e. RingOps -> U e. ran ( 2nd ` R ) )
18		eqid	|- ( 2nd ` R ) = ( 2nd ` R )
19		eqid	|- ( 1st ` R ) = ( 1st ` R )
20	18 19	rngorn1eq	|- ( R e. RingOps -> ran ( 1st ` R ) = ran ( 2nd ` R ) )
21		eqtr	|- ( ( X = ran ( 1st ` R ) /\ ran ( 1st ` R ) = ran ( 2nd ` R ) ) -> X = ran ( 2nd ` R ) )
22	21	eleq2d	|- ( ( X = ran ( 1st ` R ) /\ ran ( 1st ` R ) = ran ( 2nd ` R ) ) -> ( U e. X <-> U e. ran ( 2nd ` R ) ) )
23	1 20 22	sylancr	|- ( R e. RingOps -> ( U e. X <-> U e. ran ( 2nd ` R ) ) )
24	17 23	mpbird	|- ( R e. RingOps -> U e. X )