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 mPwSer R )
	mvrf.v	|- V = ( I mVar R )
	mvrf.b	|- B = ( Base ` S )
	mvrf.i	|- ( ph -> I e. W )
	mvrf.r	|- ( ph -> R e. Ring )
	mvrcl2.x	|- ( ph -> X e. I )
Assertion	mvrcl2	|- ( ph -> ( V ` X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		mvrf.s	|- S = ( I mPwSer R )
2		mvrf.v	|- V = ( I mVar R )
3		mvrf.b	|- B = ( Base ` S )
4		mvrf.i	|- ( ph -> I e. W )
5		mvrf.r	|- ( ph -> R e. Ring )
6		mvrcl2.x	|- ( ph -> X e. I )
7	1 2 3 4 5	mvrf	|- ( ph -> V : I --> B )
8	7 6	ffvelrnd	|- ( ph -> ( V ` X ) e. B )