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

Metamath Proof Explorer

Definition df-psr1

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

		Ref	Expression
	Assertion	df-psr1	$⊢ {PwSer}_{1} = (r \in V ⟼ (1_{𝑜} ordPwSer r) (\emptyset))$

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