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 ⊢ φ → 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