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

Metamath Proof Explorer

Theorem opsrtos

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
Assertion opsrtos ⊢ φ → O ∈ Toset

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 eqid ⊢ I mPwSer R = I mPwSer R
7 eqid ⊢ Base I mPwSer R = Base I mPwSer R
8 eqid ⊢ < R = < R
9 eqid ⊢ T < bag I = T < bag I
10 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
11 biid ⊢ ∃ z ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin x ⁡ z < R y ⁡ z ∧ ∀ w ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin w T < bag I z → x ⁡ w = y ⁡ w ↔ ∃ z ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin x ⁡ z < R y ⁡ z ∧ ∀ w ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin w T < bag I z → x ⁡ w = y ⁡ w
12 eqid ⊢ ≤ O = ≤ O
13 1 2 3 4 5 6 7 8 9 10 11 12 opsrtoslem2 ⊢ φ → O ∈ Toset