Metamath Proof Explorer


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 )