Step | Hyp | Ref
| Expression |
1 | | df-inf 8232 |
. 2
⊢ inf(𝑆, ℝ, < ) = sup(𝑆, ℝ, ◡ < ) |
2 | | gtso 9998 |
. . . 4
⊢ ◡ < Or ℝ |
3 | 2 | a1i 11 |
. . 3
⊢ ((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → ◡ < Or ℝ) |
4 | | lbcl 10853 |
. . . 4
⊢ ((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ 𝑆) |
5 | | ssel 3562 |
. . . . 5
⊢ (𝑆 ⊆ ℝ →
((℩𝑥 ∈
𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ 𝑆 → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ ℝ)) |
6 | 5 | adantr 480 |
. . . 4
⊢ ((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → ((℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ 𝑆 → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ ℝ)) |
7 | 4, 6 | mpd 15 |
. . 3
⊢ ((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ ℝ) |
8 | 7 | adantr 480 |
. . . . 5
⊢ (((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝑆) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ ℝ) |
9 | | ssel2 3563 |
. . . . . 6
⊢ ((𝑆 ⊆ ℝ ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ℝ) |
10 | 9 | adantlr 747 |
. . . . 5
⊢ (((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ ℝ) |
11 | | lble 10854 |
. . . . . 6
⊢ ((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝑧 ∈ 𝑆) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ≤ 𝑧) |
12 | 11 | 3expa 1257 |
. . . . 5
⊢ (((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝑆) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ≤ 𝑧) |
13 | 8, 10, 12 | lensymd 10067 |
. . . 4
⊢ (((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝑆) → ¬ 𝑧 < (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)) |
14 | | elex 3185 |
. . . . . . . 8
⊢
((℩𝑥
∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ 𝑆 → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ V) |
15 | 4, 14 | syl 17 |
. . . . . . 7
⊢ ((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ V) |
16 | | vex 3176 |
. . . . . . 7
⊢ 𝑧 ∈ V |
17 | | brcnvg 5225 |
. . . . . . 7
⊢
(((℩𝑥
∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∈ V ∧ 𝑧 ∈ V) → ((℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)◡
< 𝑧 ↔ 𝑧 < (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦))) |
18 | 15, 16, 17 | sylancl 693 |
. . . . . 6
⊢ ((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → ((℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)◡
< 𝑧 ↔ 𝑧 < (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦))) |
19 | 18 | notbid 307 |
. . . . 5
⊢ ((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → (¬ (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)◡
< 𝑧 ↔ ¬ 𝑧 < (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦))) |
20 | 19 | adantr 480 |
. . . 4
⊢ (((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝑆) → (¬ (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)◡
< 𝑧 ↔ ¬ 𝑧 < (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦))) |
21 | 13, 20 | mpbird 246 |
. . 3
⊢ (((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝑆) → ¬ (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)◡
< 𝑧) |
22 | 3, 7, 4, 21 | supmax 8256 |
. 2
⊢ ((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → sup(𝑆, ℝ, ◡ < ) = (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)) |
23 | 1, 22 | syl5eq 2656 |
1
⊢ ((𝑆 ⊆ ℝ ∧
∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → inf(𝑆, ℝ, < ) = (℩𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦)) |