Theorem reldvdsr

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

	Ref	Expression
Hypothesis	reldvdsr.1	|- .|| = ( ||r ` R )
Assertion	reldvdsr	|- Rel .||

Proof

Step	Hyp	Ref	Expression
1		reldvdsr.1	|- .|| = ( ||r ` R )
2		df-dvdsr	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
3	2	relmptopab	|- Rel ( ||r ` R )
4	1	releqi	|- ( Rel .|| <-> Rel ( ||r ` R ) )
5	3 4	mpbir	|- Rel .||