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	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	mvrf.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
	mvrf.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	mvrf.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mvrf.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mvrcl2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion	mvrcl2	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mvrf.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		mvrf.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
3		mvrf.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		mvrf.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		mvrf.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		mvrcl2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
7	1 2 3 4 5	mvrf	⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ 𝐵 )
8	7 6	ffvelrnd	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 )