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

Metamath Proof Explorer

Definition df-vr1

Description: Define the base element of a univariate power series (the X element of the set R [ X ] of polynomials and also the X in the set R [ [ X ] ] of power series). (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Assertion df-vr1 var1 = ( 𝑟 ∈ V ↦ ( ( 1o mVar 𝑟 ) ‘ ∅ ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cv1 ⊢ var1
1 vr ⊢ 𝑟
2 cvv ⊢ V
3 c1o ⊢ 1o
4 cmvr ⊢ mVar
5 1 cv ⊢ 𝑟
6 3 5 4 co ⊢ ( 1o mVar 𝑟 )
7 c0 ⊢ ∅
8 7 6 cfv ⊢ ( ( 1o mVar 𝑟 ) ‘ ∅ )
9 1 2 8 cmpt ⊢ ( 𝑟 ∈ V ↦ ( ( 1o mVar 𝑟 ) ‘ ∅ ) )
10 0 9 wceq ⊢ var1 = ( 𝑟 ∈ V ↦ ( ( 1o mVar 𝑟 ) ‘ ∅ ) )