This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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