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 ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) ) |