Theorem retos

Description: The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018)

	Ref	Expression
Assertion	retos	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Toset}$$

Proof

Step	Hyp	Ref	Expression
1		ltso	$$⊢<\mathrm{Or}ℝ$$
2		idref	$$⊢{\mathrm{I}\upharpoonright }_{ℝ}\subseteq \le \leftrightarrow \forall x\in ℝx\le x$$
3		leid	$$⊢x\in ℝ\to x\le x$$
4	2 3	mprgbir	$$⊢{\mathrm{I}\upharpoonright }_{ℝ}\subseteq \le$$
5		df-refld	$$⊢{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℝ$$
6	5	ovexi	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{V}$$
7		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
8		rele2	$$⊢\le ={\le }_{{ℝ}_{\mathrm{fld}}}$$
9		relt	$$⊢<={<}_{{ℝ}_{\mathrm{fld}}}$$
10	7 8 9	tosso	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{V}\to \left({ℝ}_{\mathrm{fld}}\in \mathrm{Toset}\leftrightarrow \left(<\mathrm{Or}ℝ\wedge {\mathrm{I}\upharpoonright }_{ℝ}\subseteq \le \right)\right)$$
11	6 10	ax-mp	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Toset}\leftrightarrow \left(<\mathrm{Or}ℝ\wedge {\mathrm{I}\upharpoonright }_{ℝ}\subseteq \le \right)$$
12	1 4 11	mpbir2an	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Toset}$$