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 ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplrcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion mplrcl ( 𝑋 ∈ 𝐵 → 𝐼 ∈ V )

Proof

Step Hyp Ref Expression
1 mplrcl.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplrcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 reldmmpl ⊢ Rel dom mPoly
4 1 2 3 strov2rcl ⊢ ( 𝑋 ∈ 𝐵 → 𝐼 ∈ V )