Theorem unitcl

Description: A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	unitcl.1	|- B = ( Base ` R )
	unitcl.2	|- U = ( Unit ` R )
Assertion	unitcl	|- ( X e. U -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		unitcl.1	|- B = ( Base ` R )
2		unitcl.2	|- U = ( Unit ` R )
3		eqid	|- ( 1r ` R ) = ( 1r ` R )
4		eqid	|- ( ||r ` R ) = ( ||r ` R )
5		eqid	|- ( oppR ` R ) = ( oppR ` R )
6		eqid	|- ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
7	2 3 4 5 6	isunit	|- ( X e. U <-> ( X ( ||r ` R ) ( 1r ` R ) /\ X ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
8	7	simplbi	|- ( X e. U -> X ( ||r ` R ) ( 1r ` R ) )
9	1 4	dvdsrcl	|- ( X ( ||r ` R ) ( 1r ` R ) -> X e. B )
10	8 9	syl	|- ( X e. U -> X e. B )