Theorem xrmineq

Description: The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015)

	Ref	Expression
Assertion	xrmineq	|- ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , A , B ) = B )

Proof

Step	Hyp	Ref	Expression
1		xrletri3	|- ( ( B e. RR* /\ A e. RR* ) -> ( B = A <-> ( B <_ A /\ A <_ B ) ) )
2	1	ancoms	|- ( ( A e. RR* /\ B e. RR* ) -> ( B = A <-> ( B <_ A /\ A <_ B ) ) )
3	2	biimpar	|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( B <_ A /\ A <_ B ) ) -> B = A )
4	3	anassrs	|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ B <_ A ) /\ A <_ B ) -> B = A )
5	4	ifeq1da	|- ( ( ( A e. RR* /\ B e. RR* ) /\ B <_ A ) -> if ( A <_ B , B , B ) = if ( A <_ B , A , B ) )
6	5	3impa	|- ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , B , B ) = if ( A <_ B , A , B ) )
7		ifid	|- if ( A <_ B , B , B ) = B
8	6 7	eqtr3di	|- ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , A , B ) = B )