Theorem opsrtos

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

	Ref	Expression
Hypotheses	opsrso.o	|- O = ( ( I ordPwSer R ) ` T )
	opsrso.i	|- ( ph -> I e. V )
	opsrso.r	|- ( ph -> R e. Toset )
	opsrso.t	|- ( ph -> T C_ ( I X. I ) )
	opsrso.w	|- ( ph -> T We I )
Assertion	opsrtos	|- ( ph -> O e. Toset )

Proof

Step	Hyp	Ref	Expression
1		opsrso.o	|- O = ( ( I ordPwSer R ) ` T )
2		opsrso.i	|- ( ph -> I e. V )
3		opsrso.r	|- ( ph -> R e. Toset )
4		opsrso.t	|- ( ph -> T C_ ( I X. I ) )
5		opsrso.w	|- ( ph -> T We I )
6		eqid	|- ( I mPwSer R ) = ( I mPwSer R )
7		eqid	|- ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
8		eqid	|- ( lt ` R ) = ( lt ` R )
9		eqid	|- ( T
10		eqid	|- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
11		biid	|- ( E. z e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( x ` z ) ( lt ` R ) ( y ` z ) /\ A. w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( w ( T ( x ` w ) = ( y ` w ) ) ) <-> E. z e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( x ` z ) ( lt ` R ) ( y ` z ) /\ A. w e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( w ( T ( x ` w ) = ( y ` w ) ) ) )
12		eqid	|- ( le ` O ) = ( le ` O )
13	1 2 3 4 5 6 7 8 9 10 11 12	opsrtoslem2	|- ( ph -> O e. Toset )