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 = ( PwSer1 ` R )
Assertion	psr1tos	|- ( R e. Toset -> S e. Toset )

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	|- S = ( PwSer1 ` R )
2	1	psr1val	|- S = ( ( 1o ordPwSer R ) ` (/) )
3		1on	|- 1o e. On
4	3	a1i	|- ( R e. Toset -> 1o e. On )
5		id	|- ( R e. Toset -> R e. Toset )
6		0ss	|- (/) C_ ( 1o X. 1o )
7	6	a1i	|- ( R e. Toset -> (/) C_ ( 1o X. 1o ) )
8		0we1	|- (/) We 1o
9	8	a1i	|- ( R e. Toset -> (/) We 1o )
10	2 4 5 7 9	opsrtos	|- ( R e. Toset -> S e. Toset )