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 ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrso.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
opsrso.r ⊢ ( 𝜑 → 𝑅 ∈ Toset )
opsrso.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
opsrso.w ⊢ ( 𝜑 → 𝑇 We 𝐼 )
opsrso.l ⊢ ≤ = ( lt ‘ 𝑂 )
opsrso.b ⊢ 𝐵 = ( Base ‘ 𝑂 )
Assertion opsrso ( 𝜑 → ≤ Or 𝐵 )

Proof

Step Hyp Ref Expression
1 opsrso.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
2 opsrso.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 opsrso.r ⊢ ( 𝜑 → 𝑅 ∈ Toset )
4 opsrso.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
5 opsrso.w ⊢ ( 𝜑 → 𝑇 We 𝐼 )
6 opsrso.l ⊢ ≤ = ( lt ‘ 𝑂 )
7 opsrso.b ⊢ 𝐵 = ( Base ‘ 𝑂 )
8 1 2 3 4 5 opsrtos ⊢ ( 𝜑 → 𝑂 ∈ Toset )
9 eqid ⊢ ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
10 7 9 6 tosso ⊢ ( 𝑂 ∈ Toset → ( 𝑂 ∈ Toset ↔ ( ≤ Or 𝐵 ∧ ( I ↾ 𝐵 ) ⊆ ( le ‘ 𝑂 ) ) ) )
11 10 ibi ⊢ ( 𝑂 ∈ Toset → ( ≤ Or 𝐵 ∧ ( I ↾ 𝐵 ) ⊆ ( le ‘ 𝑂 ) ) )
12 8 11 syl ⊢ ( 𝜑 → ( ≤ Or 𝐵 ∧ ( I ↾ 𝐵 ) ⊆ ( le ‘ 𝑂 ) ) )
13 12 simpld ⊢ ( 𝜑 → ≤ Or 𝐵 )