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		ifid	|- if ( A <_ B , B , B ) = B
2		xrletri3	|- ( ( B e. RR* /\ A e. RR* ) -> ( B = A <-> ( B <_ A /\ A <_ B ) ) )
3	2	ancoms	|- ( ( A e. RR* /\ B e. RR* ) -> ( B = A <-> ( B <_ A /\ A <_ B ) ) )
4	3	biimpar	|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( B <_ A /\ A <_ B ) ) -> B = A )
5	4	anassrs	|- ( ( ( ( A e. RR* /\ B e. RR* ) /\ B <_ A ) /\ A <_ B ) -> B = A )
6	5	ifeq1da	|- ( ( ( A e. RR* /\ B e. RR* ) /\ B <_ A ) -> if ( A <_ B , B , B ) = if ( A <_ B , A , B ) )
7	6	3impa	|- ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , B , B ) = if ( A <_ B , A , B ) )
8	1 7	syl5reqr	|- ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , A , B ) = B )