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 
|- <_ e. TosetRel

Proof

Step Hyp Ref Expression
1 lerel 
 |-  Rel <_
2 lerelxr 
 |-  <_ C_ ( RR* X. RR* )
3 2 brel 
 |-  ( x <_ y -> ( x e. RR* /\ y e. RR* ) )
4 3 adantr 
 |-  ( ( x <_ y /\ y <_ z ) -> ( x e. RR* /\ y e. RR* ) )
5 4 simpld 
 |-  ( ( x <_ y /\ y <_ z ) -> x e. RR* )
6 4 simprd 
 |-  ( ( x <_ y /\ y <_ z ) -> y e. RR* )
7 2 brel 
 |-  ( y <_ z -> ( y e. RR* /\ z e. RR* ) )
8 7 simprd 
 |-  ( y <_ z -> z e. RR* )
9 8 adantl 
 |-  ( ( x <_ y /\ y <_ z ) -> z e. RR* )
10 5 6 9 3jca 
 |-  ( ( x <_ y /\ y <_ z ) -> ( x e. RR* /\ y e. RR* /\ z e. RR* ) )
11 xrletr 
 |-  ( ( x e. RR* /\ y e. RR* /\ z e. RR* ) -> ( ( x <_ y /\ y <_ z ) -> x <_ z ) )
12 10 11 mpcom 
 |-  ( ( x <_ y /\ y <_ z ) -> x <_ z )
13 12 ax-gen 
 |-  A. z ( ( x <_ y /\ y <_ z ) -> x <_ z )
14 13 gen2 
 |-  A. x A. y A. z ( ( x <_ y /\ y <_ z ) -> x <_ z )
15 cotr 
 |-  ( ( <_ o. <_ ) C_ <_ <-> A. x A. y A. z ( ( x <_ y /\ y <_ z ) -> x <_ z ) )
16 14 15 mpbir 
 |-  ( <_ o. <_ ) C_ <_
17 asymref 
 |-  ( ( <_ i^i `' <_ ) = ( _I |` U. U. <_ ) <-> A. x e. U. U. <_ A. y ( ( x <_ y /\ y <_ x ) <-> x = y ) )
18 simpr 
 |-  ( ( x e. RR* /\ ( x <_ y /\ y <_ x ) ) -> ( x <_ y /\ y <_ x ) )
19 2 brel 
 |-  ( y <_ x -> ( y e. RR* /\ x e. RR* ) )
20 19 simpld 
 |-  ( y <_ x -> y e. RR* )
21 20 adantl 
 |-  ( ( x <_ y /\ y <_ x ) -> y e. RR* )
22 xrletri3 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x = y <-> ( x <_ y /\ y <_ x ) ) )
23 21 22 sylan2 
 |-  ( ( x e. RR* /\ ( x <_ y /\ y <_ x ) ) -> ( x = y <-> ( x <_ y /\ y <_ x ) ) )
24 18 23 mpbird 
 |-  ( ( x e. RR* /\ ( x <_ y /\ y <_ x ) ) -> x = y )
25 24 ex 
 |-  ( x e. RR* -> ( ( x <_ y /\ y <_ x ) -> x = y ) )
26 xrleid 
 |-  ( x e. RR* -> x <_ x )
27 26 26 jca 
 |-  ( x e. RR* -> ( x <_ x /\ x <_ x ) )
28 breq2 
 |-  ( x = y -> ( x <_ x <-> x <_ y ) )
29 breq1 
 |-  ( x = y -> ( x <_ x <-> y <_ x ) )
30 28 29 anbi12d 
 |-  ( x = y -> ( ( x <_ x /\ x <_ x ) <-> ( x <_ y /\ y <_ x ) ) )
31 27 30 syl5ibcom 
 |-  ( x e. RR* -> ( x = y -> ( x <_ y /\ y <_ x ) ) )
32 25 31 impbid 
 |-  ( x e. RR* -> ( ( x <_ y /\ y <_ x ) <-> x = y ) )
33 32 alrimiv 
 |-  ( x e. RR* -> A. y ( ( x <_ y /\ y <_ x ) <-> x = y ) )
34 lefld 
 |-  RR* = U. U. <_
35 34 eqcomi 
 |-  U. U. <_ = RR*
36 33 35 eleq2s 
 |-  ( x e. U. U. <_ -> A. y ( ( x <_ y /\ y <_ x ) <-> x = y ) )
37 17 36 mprgbir 
 |-  ( <_ i^i `' <_ ) = ( _I |` U. U. <_ )
38 xrex 
 |-  RR* e. _V
39 38 38 xpex 
 |-  ( RR* X. RR* ) e. _V
40 39 2 ssexi 
 |-  <_ e. _V
41 isps 
 |-  ( <_ e. _V -> ( <_ e. PosetRel <-> ( Rel <_ /\ ( <_ o. <_ ) C_ <_ /\ ( <_ i^i `' <_ ) = ( _I |` U. U. <_ ) ) ) )
42 40 41 ax-mp 
 |-  ( <_ e. PosetRel <-> ( Rel <_ /\ ( <_ o. <_ ) C_ <_ /\ ( <_ i^i `' <_ ) = ( _I |` U. U. <_ ) ) )
43 1 16 37 42 mpbir3an 
 |-  <_ e. PosetRel
44 xrletri 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x <_ y \/ y <_ x ) )
45 44 rgen2 
 |-  A. x e. RR* A. y e. RR* ( x <_ y \/ y <_ x )
46 qfto 
 |-  ( ( RR* X. RR* ) C_ ( <_ u. `' <_ ) <-> A. x e. RR* A. y e. RR* ( x <_ y \/ y <_ x ) )
47 45 46 mpbir 
 |-  ( RR* X. RR* ) C_ ( <_ u. `' <_ )
48 ledm 
 |-  RR* = dom <_
49 48 istsr 
 |-  ( <_ e. TosetRel <-> ( <_ e. PosetRel /\ ( RR* X. RR* ) C_ ( <_ u. `' <_ ) ) )
50 43 47 49 mpbir2an 
 |-  <_ e. TosetRel