Metamath Proof Explorer


Theorem letsr

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 TosetRel

Proof

Step Hyp Ref Expression
1 lerel Rel
2 lerelxr *×*
3 2 brel xyx*y*
4 3 adantr xyyzx*y*
5 4 simpld xyyzx*
6 4 simprd xyyzy*
7 2 brel yzy*z*
8 7 simprd yzz*
9 8 adantl xyyzz*
10 5 6 9 3jca xyyzx*y*z*
11 xrletr x*y*z*xyyzxz
12 10 11 mpcom xyyzxz
13 12 ax-gen zxyyzxz
14 13 gen2 xyzxyyzxz
15 cotr xyzxyyzxz
16 14 15 mpbir
17 asymref -1=Ixyxyyxx=y
18 simpr x*xyyxxyyx
19 2 brel yxy*x*
20 19 simpld yxy*
21 20 adantl xyyxy*
22 xrletri3 x*y*x=yxyyx
23 21 22 sylan2 x*xyyxx=yxyyx
24 18 23 mpbird x*xyyxx=y
25 24 ex x*xyyxx=y
26 xrleid x*xx
27 26 26 jca x*xxxx
28 breq2 x=yxxxy
29 breq1 x=yxxyx
30 28 29 anbi12d x=yxxxxxyyx
31 27 30 syl5ibcom x*x=yxyyx
32 25 31 impbid x*xyyxx=y
33 32 alrimiv x*yxyyxx=y
34 lefld *=
35 34 eqcomi =*
36 33 35 eleq2s xyxyyxx=y
37 17 36 mprgbir -1=I
38 xrex *V
39 38 38 xpex *×*V
40 39 2 ssexi V
41 isps VPosetRelRel-1=I
42 40 41 ax-mp PosetRelRel-1=I
43 1 16 37 42 mpbir3an PosetRel
44 xrletri x*y*xyyx
45 44 rgen2 x*y*xyyx
46 qfto *×*-1x*y*xyyx
47 45 46 mpbir *×*-1
48 ledm *=dom
49 48 istsr TosetRelPosetRel*×*-1
50 43 47 49 mpbir2an TosetRel