Theorem psr1tos

Description: The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 2-Jun-2015)

	Ref	Expression
Hypothesis	psr1val.1	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
Assertion	psr1tos	$$⊢R\in \mathrm{Toset}\to S\in \mathrm{Toset}$$

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
2	1	psr1val	$$⊢S=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
3		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
4	3	a1i	$$⊢R\in \mathrm{Toset}\to 1_{𝑜}\in \mathrm{On}$$
5		id	$$⊢R\in \mathrm{Toset}\to R\in \mathrm{Toset}$$
6		0ss	$$⊢\varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
7	6	a1i	$$⊢R\in \mathrm{Toset}\to \varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
8		0we1	$$⊢\varnothing \mathrm{We}{1}_{𝑜}$$
9	8	a1i	$$⊢R\in \mathrm{Toset}\to \varnothing \mathrm{We}{1}_{𝑜}$$
10	2 4 5 7 9	opsrtos	$$⊢R\in \mathrm{Toset}\to S\in \mathrm{Toset}$$