Description: The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | xrstos | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrsex | |
|
2 | xrsbas | |
|
3 | xrsle | |
|
4 | xrleid | |
|
5 | xrletri3 | |
|
6 | 5 | biimprd | |
7 | xrletr | |
|
8 | 1 2 3 4 6 7 | isposi | |
9 | xrletri | |
|
10 | 9 | rgen2 | |
11 | 2 3 | istos | |
12 | 8 10 11 | mpbir2an | |