Metamath Proof Explorer


Theorem dfle2

Description: Alternative definition of 'less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 6-Nov-2015)

Ref Expression
Assertion dfle2
|- <_ = ( < u. ( _I |` RR* ) )

Proof

Step Hyp Ref Expression
1 lerel
 |-  Rel <_
2 ltrelxr
 |-  < C_ ( RR* X. RR* )
3 idssxp
 |-  ( _I |` RR* ) C_ ( RR* X. RR* )
4 2 3 unssi
 |-  ( < u. ( _I |` RR* ) ) C_ ( RR* X. RR* )
5 relxp
 |-  Rel ( RR* X. RR* )
6 relss
 |-  ( ( < u. ( _I |` RR* ) ) C_ ( RR* X. RR* ) -> ( Rel ( RR* X. RR* ) -> Rel ( < u. ( _I |` RR* ) ) ) )
7 4 5 6 mp2
 |-  Rel ( < u. ( _I |` RR* ) )
8 lerelxr
 |-  <_ C_ ( RR* X. RR* )
9 8 brel
 |-  ( x <_ y -> ( x e. RR* /\ y e. RR* ) )
10 4 brel
 |-  ( x ( < u. ( _I |` RR* ) ) y -> ( x e. RR* /\ y e. RR* ) )
11 xrleloe
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x <_ y <-> ( x < y \/ x = y ) ) )
12 resieq
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x ( _I |` RR* ) y <-> x = y ) )
13 12 orbi2d
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( ( x < y \/ x ( _I |` RR* ) y ) <-> ( x < y \/ x = y ) ) )
14 11 13 bitr4d
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x <_ y <-> ( x < y \/ x ( _I |` RR* ) y ) ) )
15 brun
 |-  ( x ( < u. ( _I |` RR* ) ) y <-> ( x < y \/ x ( _I |` RR* ) y ) )
16 14 15 bitr4di
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x <_ y <-> x ( < u. ( _I |` RR* ) ) y ) )
17 9 10 16 pm5.21nii
 |-  ( x <_ y <-> x ( < u. ( _I |` RR* ) ) y )
18 1 7 17 eqbrriv
 |-  <_ = ( < u. ( _I |` RR* ) )