Metamath Proof Explorer


Theorem psr1tos

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

Ref Expression
Hypothesis psr1val.1 S=PwSer1R
Assertion psr1tos RTosetSToset

Proof

Step Hyp Ref Expression
1 psr1val.1 S=PwSer1R
2 1 psr1val S=1𝑜ordPwSerR
3 1on 1𝑜On
4 3 a1i RToset1𝑜On
5 id RTosetRToset
6 0ss 1𝑜×1𝑜
7 6 a1i RToset1𝑜×1𝑜
8 0we1 We1𝑜
9 8 a1i RTosetWe1𝑜
10 2 4 5 7 9 opsrtos RTosetSToset