This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reldvdsr

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

		Ref	Expression
	Hypothesis	reldvdsr.1	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
	Assertion	reldvdsr	$⊢ Rel \underset{˙}{∥}$

Step	Hyp	Ref	Expression
1		reldvdsr.1	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
2		df-dvdsr	$⊢ ∥_{r} = (w \in V ⟼ \{⟨x, y⟩ \| (x \in {Base}_{w} \land \exists z \in {Base}_{w} z \cdot_{w} x = y)\})$
3	2	relmptopab	$⊢ Rel ∥_{r} (R)$
4	1	releqi	$⊢ Rel \underset{˙}{∥} \leftrightarrow Rel ∥_{r} (R)$
5	3 4	mpbir	$⊢ Rel \underset{˙}{∥}$