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

Metamath Proof Explorer

Theorem dvdsrcl

Description: Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014)

Ref Expression
Hypotheses dvdsr.1 ⊢ B = Base R
dvdsr.2 ⊢ ∥ ˙ = ∥ r ⁡ R
Assertion dvdsrcl ⊢ X ∥ ˙ Y → X ∈ B

Proof

Step Hyp Ref Expression
1 dvdsr.1 ⊢ B = Base R
2 dvdsr.2 ⊢ ∥ ˙ = ∥ r ⁡ R
3 eqid ⊢ ⋅ R = ⋅ R
4 1 2 3 dvdsr ⊢ X ∥ ˙ Y ↔ X ∈ B ∧ ∃ x ∈ B x ⋅ R X = Y
5 4 simplbi ⊢ X ∥ ˙ Y → X ∈ B