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