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=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
	opsrso.i	$$⊢\phi \to I\in V$$
	opsrso.r	$$⊢\phi \to R\in \mathrm{Toset}$$
	opsrso.t	$$⊢\phi \to T\subseteq I\times I$$
	opsrso.w	$$⊢\phi \to T\mathrm{We}I$$
	opsrso.l	$$⊢\underset{\dot{}}{\le }={<}_O$$
	opsrso.b	$$⊢B={\mathrm{Base}}_O$$
Assertion	opsrso	$$⊢\phi \to \underset{\dot{}}{\le }\mathrm{Or}B$$

Proof

Step	Hyp	Ref	Expression
1		opsrso.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
2		opsrso.i	$$⊢\phi \to I\in V$$
3		opsrso.r	$$⊢\phi \to R\in \mathrm{Toset}$$
4		opsrso.t	$$⊢\phi \to T\subseteq I\times I$$
5		opsrso.w	$$⊢\phi \to T\mathrm{We}I$$
6		opsrso.l	$$⊢\underset{\dot{}}{\le }={<}_O$$
7		opsrso.b	$$⊢B={\mathrm{Base}}_O$$
8	1 2 3 4 5	opsrtos	$$⊢\phi \to O\in \mathrm{Toset}$$
9		eqid	$$⊢{\le }_O={\le }_O$$
10	7 9 6	tosso	$$⊢O\in \mathrm{Toset}\to \left(O\in \mathrm{Toset}\leftrightarrow \left(\underset{\dot{}}{\le }\mathrm{Or}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq {\le }_O\right)\right)$$
11	10	ibi	$$⊢O\in \mathrm{Toset}\to \left(\underset{\dot{}}{\le }\mathrm{Or}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq {\le }_O\right)$$
12	8 11	syl	$$⊢\phi \to \left(\underset{\dot{}}{\le }\mathrm{Or}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq {\le }_O\right)$$
13	12	simpld	$$⊢\phi \to \underset{\dot{}}{\le }\mathrm{Or}B$$