This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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* ) )