Definition df-psr1

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

	Ref	Expression
Assertion	df-psr1	$$⊢{\mathrm{PwSer}}_1=\left(r\in \mathrm{V}⟼\left(1_{𝑜}\mathrm{ordPwSer}r\right)\left(\varnothing \right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cps1	$$class{\mathrm{PwSer}}_1$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		c1o	$$class{1}_{𝑜}$$
4		copws	$$class\mathrm{ordPwSer}$$
5	1	cv	$$setvarr$$
6	3 5 4	co	$$class\left(1_{𝑜}\mathrm{ordPwSer}r\right)$$
7		c0	$$class\varnothing$$
8	7 6	cfv	$$class\left(1_{𝑜}\mathrm{ordPwSer}r\right)\left(\varnothing \right)$$
9	1 2 8	cmpt	$$class\left(r\in \mathrm{V}⟼\left(1_{𝑜}\mathrm{ordPwSer}r\right)\left(\varnothing \right)\right)$$
10	0 9	wceq	$$wff{\mathrm{PwSer}}_1=\left(r\in \mathrm{V}⟼\left(1_{𝑜}\mathrm{ordPwSer}r\right)\left(\varnothing \right)\right)$$