Theorem lemaxle

Description: A real number which is less than or equal to a second real number is less than or equal to the maximum/supremum of the second real number and a third real number. (Contributed by AV, 8-Jun-2021)

	Ref	Expression
Assertion	lemaxle	|- ( ( ( B e. RR /\ C e. RR ) /\ A e. RR /\ A <_ B ) -> A <_ if ( C <_ B , B , C ) )

Proof

Step	Hyp	Ref	Expression
1		max2	|- ( ( C e. RR /\ B e. RR ) -> B <_ if ( C <_ B , B , C ) )
2	1	ancoms	|- ( ( B e. RR /\ C e. RR ) -> B <_ if ( C <_ B , B , C ) )
3	2	adantr	|- ( ( ( B e. RR /\ C e. RR ) /\ A e. RR ) -> B <_ if ( C <_ B , B , C ) )
4		simpr	|- ( ( ( B e. RR /\ C e. RR ) /\ A e. RR ) -> A e. RR )
5		simpll	|- ( ( ( B e. RR /\ C e. RR ) /\ A e. RR ) -> B e. RR )
6		ifcl	|- ( ( B e. RR /\ C e. RR ) -> if ( C <_ B , B , C ) e. RR )
7	6	adantr	|- ( ( ( B e. RR /\ C e. RR ) /\ A e. RR ) -> if ( C <_ B , B , C ) e. RR )
8		letr	|- ( ( A e. RR /\ B e. RR /\ if ( C <_ B , B , C ) e. RR ) -> ( ( A <_ B /\ B <_ if ( C <_ B , B , C ) ) -> A <_ if ( C <_ B , B , C ) ) )
9	4 5 7 8	syl3anc	|- ( ( ( B e. RR /\ C e. RR ) /\ A e. RR ) -> ( ( A <_ B /\ B <_ if ( C <_ B , B , C ) ) -> A <_ if ( C <_ B , B , C ) ) )
10	3 9	mpan2d	|- ( ( ( B e. RR /\ C e. RR ) /\ A e. RR ) -> ( A <_ B -> A <_ if ( C <_ B , B , C ) ) )
11	10	3impia	|- ( ( ( B e. RR /\ C e. RR ) /\ A e. RR /\ A <_ B ) -> A <_ if ( C <_ B , B , C ) )