Theorem xrmaxeq

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

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

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 , A ) = if ( A <_ B , A , A ) )
6	5	3impa	|- ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , B , A ) = if ( A <_ B , A , A ) )
7		ifid	|- if ( A <_ B , A , A ) = A
8	6 7	eqtrdi	|- ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , B , A ) = A )