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 φ I V
opsrso.r φ R Toset
opsrso.t φ T I × I
opsrso.w φ T We I
opsrso.l ˙ = < O
opsrso.b B = Base O
Assertion opsrso φ ˙ Or B

Proof

Step Hyp Ref Expression
1 opsrso.o O = I ordPwSer R T
2 opsrso.i φ I V
3 opsrso.r φ R Toset
4 opsrso.t φ T I × I
5 opsrso.w φ T We I
6 opsrso.l ˙ = < O
7 opsrso.b B = Base O
8 1 2 3 4 5 opsrtos φ O Toset
9 eqid O = O
10 7 9 6 tosso O Toset O Toset ˙ Or B I B O
11 10 ibi O Toset ˙ Or B I B O
12 8 11 syl φ ˙ Or B I B O
13 12 simpld φ ˙ Or B