Theorem reldvdsr

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

	Ref	Expression
Hypothesis	reldvdsr.1	⊢ ∥ = ( ∥r ‘ 𝑅 )
Assertion	reldvdsr	⊢ Rel ∥

Proof

Step	Hyp	Ref	Expression
1		reldvdsr.1	⊢ ∥ = ( ∥r ‘ 𝑅 )
2		df-dvdsr	⊢ ∥r = ( 𝑤 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } )
3	2	relmptopab	⊢ Rel ( ∥r ‘ 𝑅 )
4	1	releqi	⊢ ( Rel ∥ ↔ Rel ( ∥r ‘ 𝑅 ) )
5	3 4	mpbir	⊢ Rel ∥