Proof of Theorem dfinfre
| Step | Hyp | Ref
| Expression |
| 1 | | df-inf 9483 |
. 2
⊢ inf(𝐴, ℝ, < ) = sup(𝐴, ℝ, ◡ < ) |
| 2 | | df-sup 9482 |
. . 3
⊢ sup(𝐴, ℝ, ◡ < ) = ∪
{𝑥 ∈ ℝ ∣
(∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧))} |
| 3 | | ssel2 3978 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
| 4 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 5 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
| 6 | 4, 5 | brcnv 5893 |
. . . . . . . . . . . 12
⊢ (𝑥◡ < 𝑦 ↔ 𝑦 < 𝑥) |
| 7 | 6 | notbii 320 |
. . . . . . . . . . 11
⊢ (¬
𝑥◡ < 𝑦 ↔ ¬ 𝑦 < 𝑥) |
| 8 | | lenlt 11339 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥)) |
| 9 | 7, 8 | bitr4id 290 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (¬
𝑥◡ < 𝑦 ↔ 𝑥 ≤ 𝑦)) |
| 10 | 3, 9 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴)) → (¬ 𝑥◡
< 𝑦 ↔ 𝑥 ≤ 𝑦)) |
| 11 | 10 | ancoms 458 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥◡ < 𝑦 ↔ 𝑥 ≤ 𝑦)) |
| 12 | 11 | an32s 652 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → (¬ 𝑥◡
< 𝑦 ↔ 𝑥 ≤ 𝑦)) |
| 13 | 12 | ralbidva 3176 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
| 14 | 5, 4 | brcnv 5893 |
. . . . . . . . 9
⊢ (𝑦◡ < 𝑥 ↔ 𝑥 < 𝑦) |
| 15 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
| 16 | 5, 15 | brcnv 5893 |
. . . . . . . . . 10
⊢ (𝑦◡ < 𝑧 ↔ 𝑧 < 𝑦) |
| 17 | 16 | rexbii 3094 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
𝐴 𝑦◡
< 𝑧 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) |
| 18 | 14, 17 | imbi12i 350 |
. . . . . . . 8
⊢ ((𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧) ↔ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
| 19 | 18 | ralbii 3093 |
. . . . . . 7
⊢
(∀𝑦 ∈
ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧) ↔
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
| 20 | 19 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ ℝ
(𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧) ↔
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
| 21 | 13, 20 | anbi12d 632 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
((∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧)) ↔
(∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
| 22 | 21 | rabbidva 3443 |
. . . 4
⊢ (𝐴 ⊆ ℝ → {𝑥 ∈ ℝ ∣
(∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧))} = {𝑥 ∈ ℝ ∣
(∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))}) |
| 23 | 22 | unieqd 4920 |
. . 3
⊢ (𝐴 ⊆ ℝ → ∪ {𝑥
∈ ℝ ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧))} = ∪ {𝑥
∈ ℝ ∣ (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))}) |
| 24 | 2, 23 | eqtrid 2789 |
. 2
⊢ (𝐴 ⊆ ℝ →
sup(𝐴, ℝ, ◡ < ) = ∪
{𝑥 ∈ ℝ ∣
(∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))}) |
| 25 | 1, 24 | eqtrid 2789 |
1
⊢ (𝐴 ⊆ ℝ →
inf(𝐴, ℝ, < ) =
∪ {𝑥 ∈ ℝ ∣ (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))}) |