This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑆 = ( 𝐼 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 ffvelcdmd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ 𝐵 )