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	|- ( ph -> I e. V )
	opsrso.r	|- ( ph -> R e. Toset )
	opsrso.t	|- ( ph -> T C_ ( I X. I ) )
	opsrso.w	|- ( ph -> T We I )
	opsrso.l	|- .<_ = ( lt ` O )
	opsrso.b	|- B = ( Base ` O )
Assertion	opsrso	|- ( ph -> .<_ Or B )

Proof

Step	Hyp	Ref	Expression
1		opsrso.o	|- O = ( ( I ordPwSer R ) ` T )
2		opsrso.i	|- ( ph -> I e. V )
3		opsrso.r	|- ( ph -> R e. Toset )
4		opsrso.t	|- ( ph -> T C_ ( I X. I ) )
5		opsrso.w	|- ( ph -> T We I )
6		opsrso.l	|- .<_ = ( lt ` O )
7		opsrso.b	|- B = ( Base ` O )
8	1 2 3 4 5	opsrtos	|- ( ph -> O e. Toset )
9		eqid	|- ( le ` O ) = ( le ` O )
10	7 9 6	tosso	|- ( O e. Toset -> ( O e. Toset <-> ( .<_ Or B /\ ( _I |` B ) C_ ( le ` O ) ) ) )
11	10	ibi	|- ( O e. Toset -> ( .<_ Or B /\ ( _I |` B ) C_ ( le ` O ) ) )
12	8 11	syl	|- ( ph -> ( .<_ Or B /\ ( _I |` B ) C_ ( le ` O ) ) )
13	12	simpld	|- ( ph -> .<_ Or B )