Theorem dvdsrcl

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

	Ref	Expression
Hypotheses	dvdsr.1	$$⊢B={\mathrm{Base}}_R$$
	dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
Assertion	dvdsrcl	$$⊢X\underset{\dot{}}{\parallel }Y\to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		dvdsr.1	$$⊢B={\mathrm{Base}}_R$$
2		dvdsr.2	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
3		eqid	$$⊢{\cdot }_R={\cdot }_R$$
4	1 2 3	dvdsr	$$⊢X\underset{\dot{}}{\parallel }Y\leftrightarrow \left(X\in B\wedge \exists x\in Bx{\cdot }_{R}X=Y\right)$$
5	4	simplbi	$$⊢X\underset{\dot{}}{\parallel }Y\to X\in B$$