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	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
Assertion	psr1tos	⊢ ( 𝑅 ∈ Toset → 𝑆 ∈ Toset )

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
2	1	psr1val	⊢ 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
3		1on	⊢ 1o ∈ On
4	3	a1i	⊢ ( 𝑅 ∈ Toset → 1o ∈ On )
5		id	⊢ ( 𝑅 ∈ Toset → 𝑅 ∈ Toset )
6		0ss	⊢ ∅ ⊆ ( 1o × 1o )
7	6	a1i	⊢ ( 𝑅 ∈ Toset → ∅ ⊆ ( 1o × 1o ) )
8		0we1	⊢ ∅ We 1o
9	8	a1i	⊢ ( 𝑅 ∈ Toset → ∅ We 1o )
10	2 4 5 7 9	opsrtos	⊢ ( 𝑅 ∈ Toset → 𝑆 ∈ Toset )