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 =𝑠*
4 xrleid x*xx
5 xrletri3 x*y*x=yxyyx
6 5 biimprd x*y*xyyxx=y
7 xrletr x*y*z*xyyzxz
8 1 2 3 4 6 7 isposi 𝑠*Poset
9 xrletri x*y*xyyx
10 9 rgen2 x*y*xyyx
11 2 3 istos 𝑠*Toset𝑠*Posetx*y*xyyx
12 8 10 11 mpbir2an 𝑠*Toset