Theorem xrstos

Description: The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018)

	Ref	Expression
Assertion	xrstos	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{Toset}$$

Proof

Step	Hyp	Ref	Expression
1		xrsex	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{V}$$
2		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
3		xrsle	$$⊢\le ={\le }_{{ℝ}_{𝑠}^{*}}$$
4		xrleid	$$⊢x\in {ℝ}^{*}\to x\le x$$
5		xrletri3	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(x=y\leftrightarrow \left(x\le y\wedge y\le x\right)\right)$$
6	5	biimprd	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(\left(x\le y\wedge y\le x\right)\to x=y\right)$$
7		xrletr	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\wedge z\in {ℝ}^{*}\right)\to \left(\left(x\le y\wedge y\le z\right)\to x\le z\right)$$
8	1 2 3 4 6 7	isposi	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{Poset}$$
9		xrletri	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(x\le y\vee y\le x\right)$$
10	9	rgen2	$$⊢\forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\left(x\le y\vee y\le x\right)$$
11	2 3	istos	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{Toset}\leftrightarrow \left({ℝ}_{𝑠}^{*}\in \mathrm{Poset}\wedge \forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\left(x\le y\vee y\le x\right)\right)$$
12	8 10 11	mpbir2an	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{Toset}$$