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\mathrm{mPoly}R$$
	mplrcl.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	mplrcl	$$⊢X\in B\to I\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		mplrcl.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplrcl.b	$$⊢B={\mathrm{Base}}_P$$
3		reldmmpl	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPoly}$$
4	1 2 3	strov2rcl	$$⊢X\in B\to I\in \mathrm{V}$$