Theorem xrsle

Description: The ordering of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Assertion	xrsle	|- <_ = ( le ` RR*s )

Proof

Step	Hyp	Ref	Expression
1		xrex	|- RR* e. _V
2	1 1	xpex	|- ( RR* X. RR* ) e. _V
3		lerelxr	|- <_ C_ ( RR* X. RR* )
4	2 3	ssexi	|- <_ e. _V
5		df-xrs	|- RR*s = ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , *e >. } u. { <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } )
6	5	odrngle	|- ( <_ e. _V -> <_ = ( le ` RR*s ) )
7	4 6	ax-mp	|- <_ = ( le ` RR*s )