Proof of Theorem dfinfre
Step | Hyp | Ref
| Expression |
1 | | df-inf 6398 |
. 2
⊢ inf(𝐴, ℝ, < ) = sup(𝐴, ℝ, ◡ < ) |
2 | | df-sup 6397 |
. . 3
⊢ sup(𝐴, ℝ, ◡ < ) = ∪
{𝑥 ∈ ℝ ∣
(∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧))} |
3 | | ssel2 2994 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
4 | | lenlt 7187 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥)) |
5 | | vex 2604 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
6 | | vex 2604 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
7 | 5, 6 | brcnv 4536 |
. . . . . . . . . . . 12
⊢ (𝑥◡ < 𝑦 ↔ 𝑦 < 𝑥) |
8 | 7 | notbii 626 |
. . . . . . . . . . 11
⊢ (¬
𝑥◡ < 𝑦 ↔ ¬ 𝑦 < 𝑥) |
9 | 4, 8 | syl6rbbr 197 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (¬
𝑥◡ < 𝑦 ↔ 𝑥 ≤ 𝑦)) |
10 | 3, 9 | sylan2 280 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴)) → (¬ 𝑥◡
< 𝑦 ↔ 𝑥 ≤ 𝑦)) |
11 | 10 | ancoms 264 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥◡ < 𝑦 ↔ 𝑥 ≤ 𝑦)) |
12 | 11 | an32s 532 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → (¬ 𝑥◡
< 𝑦 ↔ 𝑥 ≤ 𝑦)) |
13 | 12 | ralbidva 2364 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) |
14 | 6, 5 | brcnv 4536 |
. . . . . . . . 9
⊢ (𝑦◡ < 𝑥 ↔ 𝑥 < 𝑦) |
15 | | vex 2604 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
16 | 6, 15 | brcnv 4536 |
. . . . . . . . . 10
⊢ (𝑦◡ < 𝑧 ↔ 𝑧 < 𝑦) |
17 | 16 | rexbii 2373 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
𝐴 𝑦◡
< 𝑧 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) |
18 | 14, 17 | imbi12i 237 |
. . . . . . . 8
⊢ ((𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧) ↔ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
19 | 18 | ralbii 2372 |
. . . . . . 7
⊢
(∀𝑦 ∈
ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧) ↔
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
20 | 19 | a1i 9 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ ℝ
(𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧) ↔
∀𝑦 ∈ ℝ
(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
21 | 13, 20 | anbi12d 456 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
((∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧)) ↔
(∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
22 | 21 | rabbidva 2592 |
. . . 4
⊢ (𝐴 ⊆ ℝ → {𝑥 ∈ ℝ ∣
(∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧))} = {𝑥 ∈ ℝ ∣
(∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))}) |
23 | 22 | unieqd 3612 |
. . 3
⊢ (𝐴 ⊆ ℝ → ∪ {𝑥
∈ ℝ ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥◡
< 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡
< 𝑧))} = ∪ {𝑥
∈ ℝ ∣ (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))}) |
24 | 2, 23 | syl5eq 2125 |
. 2
⊢ (𝐴 ⊆ ℝ →
sup(𝐴, ℝ, ◡ < ) = ∪
{𝑥 ∈ ℝ ∣
(∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))}) |
25 | 1, 24 | syl5eq 2125 |
1
⊢ (𝐴 ⊆ ℝ →
inf(𝐴, ℝ, < ) =
∪ {𝑥 ∈ ℝ ∣ (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))}) |