xrstos

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

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

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

Metamath Proof Explorer