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