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

Metamath Proof Explorer

Theorem mplrcl

Description: Reverse closure for the polynomial index set. (Contributed by Stefan O'Rear, 19-Mar-2015) (Revised by Mario Carneiro, 30-Aug-2015)

Ref Expression
Hypotheses mplrcl.p ⊢ P = I mPoly R
mplrcl.b ⊢ B = Base P
Assertion mplrcl ⊢ X ∈ B → I ∈ V

Proof

Step Hyp Ref Expression
1 mplrcl.p ⊢ P = I mPoly R
2 mplrcl.b ⊢ B = Base P
3 reldmmpl ⊢ Rel ⁡ dom ⁡ mPoly
4 1 2 3 strov2rcl ⊢ X ∈ B → I ∈ V