Theorem xrstos

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

	Ref	Expression
Assertion	xrstos	⊢ ℝ*𝑠 ∈ Toset

Proof

Step	Hyp	Ref	Expression
1		xrsex	⊢ ℝ*𝑠 ∈ V
2		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
3		xrsle	⊢ ≤ = ( le ‘ ℝ*𝑠 )
4		xrleid	⊢ ( 𝑥 ∈ ℝ* → 𝑥 ≤ 𝑥 )
5		xrletri3	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 = 𝑦 ↔ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) )
6	5	biimprd	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
7		xrletr	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
8	1 2 3 4 6 7	isposi	⊢ ℝ*𝑠 ∈ Poset
9		xrletri	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
10	9	rgen2	⊢ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 )
11	2 3	istos	⊢ ( ℝ*𝑠 ∈ Toset ↔ ( ℝ*𝑠 ∈ Poset ∧ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) )
12	8 10 11	mpbir2an	⊢ ℝ*𝑠 ∈ Toset