Metamath Proof Explorer

Theorem dvdszrcl

Description: Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015)

		Ref	Expression
	Assertion	dvdszrcl	$⊢ X ∥ Y \to (X \in ℤ \land Y \in ℤ)$

Step	Hyp	Ref	Expression
1		df-dvds	$⊢ ∥ = \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists z \in ℤ z x = y)\}$
2		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in ℤ \land y \in ℤ) \land \exists z \in ℤ z x = y)\} \subseteq ℤ \times ℤ$
3	1 2	eqsstri	$⊢ ∥ \subseteq ℤ \times ℤ$
4	3	brel	$⊢ X ∥ Y \to (X \in ℤ \land Y \in ℤ)$