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 )