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 e. B -> I e. _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 e. B -> I e. _V )