Description: The "less than or equal to" relationship on the extended reals is a toset. (Contributed by FL, 2-Aug-2009) (Revised by Mario Carneiro, 3-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | letsr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lerel | |
|
2 | lerelxr | |
|
3 | 2 | brel | |
4 | 3 | adantr | |
5 | 4 | simpld | |
6 | 4 | simprd | |
7 | 2 | brel | |
8 | 7 | simprd | |
9 | 8 | adantl | |
10 | 5 6 9 | 3jca | |
11 | xrletr | |
|
12 | 10 11 | mpcom | |
13 | 12 | ax-gen | |
14 | 13 | gen2 | |
15 | cotr | |
|
16 | 14 15 | mpbir | |
17 | asymref | |
|
18 | simpr | |
|
19 | 2 | brel | |
20 | 19 | simpld | |
21 | 20 | adantl | |
22 | xrletri3 | |
|
23 | 21 22 | sylan2 | |
24 | 18 23 | mpbird | |
25 | 24 | ex | |
26 | xrleid | |
|
27 | 26 26 | jca | |
28 | breq2 | |
|
29 | breq1 | |
|
30 | 28 29 | anbi12d | |
31 | 27 30 | syl5ibcom | |
32 | 25 31 | impbid | |
33 | 32 | alrimiv | |
34 | lefld | |
|
35 | 34 | eqcomi | |
36 | 33 35 | eleq2s | |
37 | 17 36 | mprgbir | |
38 | xrex | |
|
39 | 38 38 | xpex | |
40 | 39 2 | ssexi | |
41 | isps | |
|
42 | 40 41 | ax-mp | |
43 | 1 16 37 42 | mpbir3an | |
44 | xrletri | |
|
45 | 44 | rgen2 | |
46 | qfto | |
|
47 | 45 46 | mpbir | |
48 | ledm | |
|
49 | 48 | istsr | |
50 | 43 47 49 | mpbir2an | |