Metamath Proof Explorer

Theorem dflt2

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

Ref Expression
Assertion dflt2 
|- < = ( <_ \ _I )

Proof

Step Hyp Ref Expression
1 ltrel 
 |-  Rel <
2 difss 
 |-  ( <_ \ _I ) C_ <_
3 lerel 
 |-  Rel <_
4 relss 
 |-  ( ( <_ \ _I ) C_ <_ -> ( Rel <_ -> Rel ( <_ \ _I ) ) )
5 2 3 4 mp2 
 |-  Rel ( <_ \ _I )
6 ltrelxr 
 |-  < C_ ( RR* X. RR* )
7 6 brel 
 |-  ( x < y -> ( x e. RR* /\ y e. RR* ) )
8 lerelxr 
 |-  <_ C_ ( RR* X. RR* )
9 2 8 sstri 
 |-  ( <_ \ _I ) C_ ( RR* X. RR* )
10 9 brel 
 |-  ( x ( <_ \ _I ) y -> ( x e. RR* /\ y e. RR* ) )
11 xrltlen 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x < y <-> ( x <_ y /\ y =/= x ) ) )
12 equcom 
 |-  ( y = x <-> x = y )
13 vex 
 |-  y e. _V
14 13 ideq 
 |-  ( x _I y <-> x = y )
15 12 14 bitr4i 
 |-  ( y = x <-> x _I y )
16 15 necon3abii 
 |-  ( y =/= x <-> -. x _I y )
17 16 anbi2i 
 |-  ( ( x <_ y /\ y =/= x ) <-> ( x <_ y /\ -. x _I y ) )
18 11 17 bitrdi 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x < y <-> ( x <_ y /\ -. x _I y ) ) )
19 brdif 
 |-  ( x ( <_ \ _I ) y <-> ( x <_ y /\ -. x _I y ) )
20 18 19 bitr4di 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x < y <-> x ( <_ \ _I ) y ) )
21 7 10 20 pm5.21nii 
 |-  ( x < y <-> x ( <_ \ _I ) y )
22 1 5 21 eqbrriv 
 |-  < = ( <_ \ _I )