Theorem opsrtos

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$$
Assertion	opsrtos	$$⊢\phi \to O\in \mathrm{Toset}$$

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		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
7		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
8		eqid	$$⊢{<}_R={<}_R$$
9		eqid	$$⊢T{<}_{bag}I=T{<}_{bag}I$$
10		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
11		biid	$$⊢\exists z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(x\left(z\right){<}_{R}y\left(z\right)\wedge \forall w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(w\left(T{<}_{bag}I\right)z\to x\left(w\right)=y\left(w\right)\right)\right)\leftrightarrow \exists z\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(x\left(z\right){<}_{R}y\left(z\right)\wedge \forall w\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(w\left(T{<}_{bag}I\right)z\to x\left(w\right)=y\left(w\right)\right)\right)$$
12		eqid	$$⊢{\le }_O={\le }_O$$
13	1 2 3 4 5 6 7 8 9 10 11 12	opsrtoslem2	$$⊢\phi \to O\in \mathrm{Toset}$$