Theorem mvrcl2

Description: A power series variable is an element of the base set. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	mvrf.s	$$⊢S=I\mathrm{mPwSer}R$$
	mvrf.v	$$⊢V=I\mathrm{mVar}R$$
	mvrf.b	$$⊢B={\mathrm{Base}}_S$$
	mvrf.i	$$⊢\phi \to I\in W$$
	mvrf.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mvrcl2.x	$$⊢\phi \to X\in I$$
Assertion	mvrcl2	$$⊢\phi \to V\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		mvrf.s	$$⊢S=I\mathrm{mPwSer}R$$
2		mvrf.v	$$⊢V=I\mathrm{mVar}R$$
3		mvrf.b	$$⊢B={\mathrm{Base}}_S$$
4		mvrf.i	$$⊢\phi \to I\in W$$
5		mvrf.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		mvrcl2.x	$$⊢\phi \to X\in I$$
7	1 2 3 4 5	mvrf	$$⊢\phi \to V:I⟶B$$
8	7 6	ffvelrnd	$$⊢\phi \to V\left(X\right)\in B$$