Definition df-psr1

Description: Define the algebra of univariate power series. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Assertion	df-psr1	⊢ PwSer1 = ( 𝑟 ∈ V ↦ ( ( 1o ordPwSer 𝑟 ) ‘ ∅ ) )

Detailed syntax breakdown

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