Theorem 2resupmax

Description: The supremum of two real numbers is the maximum of these two numbers. (Contributed by AV, 8-Jun-2021)

	Ref	Expression
Assertion	2resupmax	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → sup ( { 𝐴 , 𝐵 } , ℝ , < ) = if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ltso	⊢ < Or ℝ
2		suppr	⊢ ( ( < Or ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → sup ( { 𝐴 , 𝐵 } , ℝ , < ) = if ( 𝐵 < 𝐴 , 𝐴 , 𝐵 ) )
3	1 2	mp3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → sup ( { 𝐴 , 𝐵 } , ℝ , < ) = if ( 𝐵 < 𝐴 , 𝐴 , 𝐵 ) )
4		ifnot	⊢ if ( ¬ 𝐵 < 𝐴 , 𝐵 , 𝐴 ) = if ( 𝐵 < 𝐴 , 𝐴 , 𝐵 )
5		lenlt	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
6	5	bicomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ¬ 𝐵 < 𝐴 ↔ 𝐴 ≤ 𝐵 ) )
7	6	ifbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ¬ 𝐵 < 𝐴 , 𝐵 , 𝐴 ) = if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) )
8	4 7	eqtr3id	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( 𝐵 < 𝐴 , 𝐴 , 𝐵 ) = if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) )
9	3 8	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → sup ( { 𝐴 , 𝐵 } , ℝ , < ) = if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) )