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

Metamath Proof Explorer

Theorem opsrso

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 )
opsrso.l 
|- .<_ = ( lt ` O )
opsrso.b 
|- B = ( Base ` O )
Assertion opsrso 
|- ( ph -> .<_ Or B )

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 opsrso.l 
 |-  .<_ = ( lt ` O )
7 opsrso.b 
 |-  B = ( Base ` O )
8 1 2 3 4 5 opsrtos 
 |-  ( ph -> O e. Toset )
9 eqid 
 |-  ( le ` O ) = ( le ` O )
10 7 9 6 tosso 
 |-  ( O e. Toset -> ( O e. Toset <-> ( .<_ Or B /\ ( _I |` B ) C_ ( le ` O ) ) ) )
11 10 ibi 
 |-  ( O e. Toset -> ( .<_ Or B /\ ( _I |` B ) C_ ( le ` O ) ) )
12 8 11 syl 
 |-  ( ph -> ( .<_ Or B /\ ( _I |` B ) C_ ( le ` O ) ) )
13 12 simpld 
 |-  ( ph -> .<_ Or B )