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

Metamath Proof Explorer

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 )