Theorem dvdsrcl

Description: Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014)

	Ref	Expression
Hypotheses	dvdsr.1	|- B = ( Base ` R )
	dvdsr.2	|- .|| = ( ||r ` R )
Assertion	dvdsrcl	|- ( X .|| Y -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	|- B = ( Base ` R )
2		dvdsr.2	|- .|| = ( ||r ` R )
3		eqid	|- ( .r ` R ) = ( .r ` R )
4	1 2 3	dvdsr	|- ( X .|| Y <-> ( X e. B /\ E. x e. B ( x ( .r ` R ) X ) = Y ) )
5	4	simplbi	|- ( X .|| Y -> X e. B )