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 𝐵 )