Step | Hyp | Ref
| Expression |
1 | | lttri3 7988 |
. . . 4
⊢ ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓))) |
2 | 1 | adantl 275 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓))) |
3 | | simplr 525 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ) |
4 | | prid2g 3686 |
. . . 4
⊢ (𝐵 ∈ ℝ → 𝐵 ∈ {𝐴, 𝐵}) |
5 | 3, 4 | syl 14 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ {𝐴, 𝐵}) |
6 | | simpll 524 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ) |
7 | 6 | ad2antrr 485 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) ∧ 𝑦 = 𝐴) → 𝐴 ∈ ℝ) |
8 | 3 | ad2antrr 485 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) ∧ 𝑦 = 𝐴) → 𝐵 ∈ ℝ) |
9 | | simpllr 529 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) ∧ 𝑦 = 𝐴) → 𝐴 ≤ 𝐵) |
10 | 7, 8, 9 | lensymd 8030 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) ∧ 𝑦 = 𝐴) → ¬ 𝐵 < 𝐴) |
11 | | breq2 3991 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝐵 < 𝑦 ↔ 𝐵 < 𝐴)) |
12 | 11 | notbid 662 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (¬ 𝐵 < 𝑦 ↔ ¬ 𝐵 < 𝐴)) |
13 | 12 | adantl 275 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) ∧ 𝑦 = 𝐴) → (¬ 𝐵 < 𝑦 ↔ ¬ 𝐵 < 𝐴)) |
14 | 10, 13 | mpbird 166 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) ∧ 𝑦 = 𝐴) → ¬ 𝐵 < 𝑦) |
15 | 3 | ad2antrr 485 |
. . . . . 6
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) ∧ 𝑦 = 𝐵) → 𝐵 ∈ ℝ) |
16 | 15 | ltnrd 8020 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) ∧ 𝑦 = 𝐵) → ¬ 𝐵 < 𝐵) |
17 | | breq2 3991 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐵 < 𝑦 ↔ 𝐵 < 𝐵)) |
18 | 17 | notbid 662 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (¬ 𝐵 < 𝑦 ↔ ¬ 𝐵 < 𝐵)) |
19 | 18 | adantl 275 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) ∧ 𝑦 = 𝐵) → (¬ 𝐵 < 𝑦 ↔ ¬ 𝐵 < 𝐵)) |
20 | 16, 19 | mpbird 166 |
. . . 4
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) ∧ 𝑦 = 𝐵) → ¬ 𝐵 < 𝑦) |
21 | | elpri 3604 |
. . . . 5
⊢ (𝑦 ∈ {𝐴, 𝐵} → (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) |
22 | 21 | adantl 275 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) → (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) |
23 | 14, 20, 22 | mpjaodan 793 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑦 ∈ {𝐴, 𝐵}) → ¬ 𝐵 < 𝑦) |
24 | 2, 3, 5, 23 | supmaxti 6978 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵) |
25 | 24 | ex 114 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 → sup({𝐴, 𝐵}, ℝ, < ) = 𝐵)) |