Metamath Proof Explorer

Theorem xrstos

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

Ref Expression
Assertion xrstos 
|- RR*s e. Toset

Proof

Step Hyp Ref Expression
1 xrsex 
 |-  RR*s e. _V
2 xrsbas 
 |-  RR* = ( Base ` RR*s )
3 xrsle 
 |-  <_ = ( le ` RR*s )
4 xrleid 
 |-  ( x e. RR* -> x <_ x )
5 xrletri3 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x = y <-> ( x <_ y /\ y <_ x ) ) )
6 5 biimprd 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( ( x <_ y /\ y <_ x ) -> x = y ) )
7 xrletr 
 |-  ( ( x e. RR* /\ y e. RR* /\ z e. RR* ) -> ( ( x <_ y /\ y <_ z ) -> x <_ z ) )
8 1 2 3 4 6 7 isposi 
 |-  RR*s e. Poset
9 xrletri 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x <_ y \/ y <_ x ) )
10 9 rgen2 
 |-  A. x e. RR* A. y e. RR* ( x <_ y \/ y <_ x )
11 2 3 istos 
 |-  ( RR*s e. Toset <-> ( RR*s e. Poset /\ A. x e. RR* A. y e. RR* ( x <_ y \/ y <_ x ) ) )
12 8 10 11 mpbir2an 
 |-  RR*s e. Toset