Theorem reldvdsr

Description: The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypothesis	reldvdsr.1	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
Assertion	reldvdsr	$$⊢\mathrm{Rel}\underset{\dot{}}{\parallel }$$

Proof

Step	Hyp	Ref	Expression
1		reldvdsr.1	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
2		df-dvdsr	$$⊢{\parallel }_r=\left(w\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(x\in {\mathrm{Base}}_w\wedge \exists z\in {\mathrm{Base}}_{w}z{\cdot }_{w}x=y\right)\right\}\right)$$
3	2	relmptopab	$$⊢\mathrm{Rel}{\parallel }_r\left(R\right)$$
4	1	releqi	$$⊢\mathrm{Rel}\underset{\dot{}}{\parallel }\leftrightarrow \mathrm{Rel}{\parallel }_r\left(R\right)$$
5	3 4	mpbir	$$⊢\mathrm{Rel}\underset{\dot{}}{\parallel }$$