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 )