Description: The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | xrsp1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrsex | |
|
2 | xrsbas | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | 2 3 4 | p1val | |
6 | 1 5 | ax-mp | |
7 | ssid | |
|
8 | xrslt | |
|
9 | xrstos | |
|
10 | 9 | a1i | |
11 | id | |
|
12 | 2 8 10 11 | toslub | |
13 | 7 12 | ax-mp | |
14 | xrsup | |
|
15 | 6 13 14 | 3eqtrri | |