Step | Hyp | Ref
| Expression |
1 | | ssel 3910 |
. . . . . . . . 9
⊢ (𝐴 ⊆ ℝ → (𝑣 ∈ 𝐴 → 𝑣 ∈ ℝ)) |
2 | 1 | pm4.71rd 562 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ → (𝑣 ∈ 𝐴 ↔ (𝑣 ∈ ℝ ∧ 𝑣 ∈ 𝐴))) |
3 | 2 | exbidv 1925 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(∃𝑣 𝑣 ∈ 𝐴 ↔ ∃𝑣(𝑣 ∈ ℝ ∧ 𝑣 ∈ 𝐴))) |
4 | | df-rex 3069 |
. . . . . . . 8
⊢
(∃𝑣 ∈
ℝ 𝑣 ∈ 𝐴 ↔ ∃𝑣(𝑣 ∈ ℝ ∧ 𝑣 ∈ 𝐴)) |
5 | | renegcl 11214 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℝ → -𝑤 ∈
ℝ) |
6 | | infm3lem 11863 |
. . . . . . . . 9
⊢ (𝑣 ∈ ℝ →
∃𝑤 ∈ ℝ
𝑣 = -𝑤) |
7 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑣 = -𝑤 → (𝑣 ∈ 𝐴 ↔ -𝑤 ∈ 𝐴)) |
8 | 5, 6, 7 | rexxfr 5334 |
. . . . . . . 8
⊢
(∃𝑣 ∈
ℝ 𝑣 ∈ 𝐴 ↔ ∃𝑤 ∈ ℝ -𝑤 ∈ 𝐴) |
9 | 4, 8 | bitr3i 276 |
. . . . . . 7
⊢
(∃𝑣(𝑣 ∈ ℝ ∧ 𝑣 ∈ 𝐴) ↔ ∃𝑤 ∈ ℝ -𝑤 ∈ 𝐴) |
10 | 3, 9 | bitrdi 286 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
(∃𝑣 𝑣 ∈ 𝐴 ↔ ∃𝑤 ∈ ℝ -𝑤 ∈ 𝐴)) |
11 | | n0 4277 |
. . . . . 6
⊢ (𝐴 ≠ ∅ ↔
∃𝑣 𝑣 ∈ 𝐴) |
12 | | rabn0 4316 |
. . . . . 6
⊢ ({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ≠ ∅ ↔ ∃𝑤 ∈ ℝ -𝑤 ∈ 𝐴) |
13 | 10, 11, 12 | 3bitr4g 313 |
. . . . 5
⊢ (𝐴 ⊆ ℝ → (𝐴 ≠ ∅ ↔ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ≠ ∅)) |
14 | | ssel 3910 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ ℝ → (𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ)) |
15 | 14 | pm4.71rd 562 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ ℝ → (𝑦 ∈ 𝐴 ↔ (𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴))) |
16 | 15 | imbi1d 341 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℝ → ((𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦) ↔ ((𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑥 ≤ 𝑦))) |
17 | | impexp 450 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑥 ≤ 𝑦) ↔ (𝑦 ∈ ℝ → (𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦))) |
18 | 16, 17 | bitrdi 286 |
. . . . . . . . 9
⊢ (𝐴 ⊆ ℝ → ((𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦) ↔ (𝑦 ∈ ℝ → (𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦)))) |
19 | 18 | albidv 1924 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ →
(∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦) ↔ ∀𝑦(𝑦 ∈ ℝ → (𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦)))) |
20 | | df-ral 3068 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 𝑥 ≤ 𝑦 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦)) |
21 | | renegcl 11214 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ℝ → -𝑣 ∈
ℝ) |
22 | | infm3lem 11863 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ →
∃𝑣 ∈ ℝ
𝑦 = -𝑣) |
23 | | eleq1 2826 |
. . . . . . . . . . 11
⊢ (𝑦 = -𝑣 → (𝑦 ∈ 𝐴 ↔ -𝑣 ∈ 𝐴)) |
24 | | breq2 5074 |
. . . . . . . . . . 11
⊢ (𝑦 = -𝑣 → (𝑥 ≤ 𝑦 ↔ 𝑥 ≤ -𝑣)) |
25 | 23, 24 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑣 → ((𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦) ↔ (-𝑣 ∈ 𝐴 → 𝑥 ≤ -𝑣))) |
26 | 21, 22, 25 | ralxfr 5332 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
ℝ (𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦) ↔ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → 𝑥 ≤ -𝑣)) |
27 | | df-ral 3068 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
ℝ (𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦) ↔ ∀𝑦(𝑦 ∈ ℝ → (𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦))) |
28 | 26, 27 | bitr3i 276 |
. . . . . . . 8
⊢
(∀𝑣 ∈
ℝ (-𝑣 ∈ 𝐴 → 𝑥 ≤ -𝑣) ↔ ∀𝑦(𝑦 ∈ ℝ → (𝑦 ∈ 𝐴 → 𝑥 ≤ 𝑦))) |
29 | 19, 20, 28 | 3bitr4g 313 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → 𝑥 ≤ -𝑣))) |
30 | 29 | rexbidv 3225 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℝ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → 𝑥 ≤ -𝑣))) |
31 | | renegcl 11214 |
. . . . . . . 8
⊢ (𝑢 ∈ ℝ → -𝑢 ∈
ℝ) |
32 | | infm3lem 11863 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
∃𝑢 ∈ ℝ
𝑥 = -𝑢) |
33 | | breq1 5073 |
. . . . . . . . . 10
⊢ (𝑥 = -𝑢 → (𝑥 ≤ -𝑣 ↔ -𝑢 ≤ -𝑣)) |
34 | 33 | imbi2d 340 |
. . . . . . . . 9
⊢ (𝑥 = -𝑢 → ((-𝑣 ∈ 𝐴 → 𝑥 ≤ -𝑣) ↔ (-𝑣 ∈ 𝐴 → -𝑢 ≤ -𝑣))) |
35 | 34 | ralbidv 3120 |
. . . . . . . 8
⊢ (𝑥 = -𝑢 → (∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → 𝑥 ≤ -𝑣) ↔ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → -𝑢 ≤ -𝑣))) |
36 | 31, 32, 35 | rexxfr 5334 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℝ ∀𝑣 ∈
ℝ (-𝑣 ∈ 𝐴 → 𝑥 ≤ -𝑣) ↔ ∃𝑢 ∈ ℝ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → -𝑢 ≤ -𝑣)) |
37 | | negeq 11143 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑣 → -𝑤 = -𝑣) |
38 | 37 | eleq1d 2823 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑣 → (-𝑤 ∈ 𝐴 ↔ -𝑣 ∈ 𝐴)) |
39 | 38 | elrab 3617 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ (𝑣 ∈ ℝ ∧ -𝑣 ∈ 𝐴)) |
40 | 39 | imbi1i 349 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → 𝑣 ≤ 𝑢) ↔ ((𝑣 ∈ ℝ ∧ -𝑣 ∈ 𝐴) → 𝑣 ≤ 𝑢)) |
41 | | impexp 450 |
. . . . . . . . . . . 12
⊢ (((𝑣 ∈ ℝ ∧ -𝑣 ∈ 𝐴) → 𝑣 ≤ 𝑢) ↔ (𝑣 ∈ ℝ → (-𝑣 ∈ 𝐴 → 𝑣 ≤ 𝑢))) |
42 | 40, 41 | bitri 274 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → 𝑣 ≤ 𝑢) ↔ (𝑣 ∈ ℝ → (-𝑣 ∈ 𝐴 → 𝑣 ≤ 𝑢))) |
43 | 42 | albii 1823 |
. . . . . . . . . 10
⊢
(∀𝑣(𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → 𝑣 ≤ 𝑢) ↔ ∀𝑣(𝑣 ∈ ℝ → (-𝑣 ∈ 𝐴 → 𝑣 ≤ 𝑢))) |
44 | | df-ral 3068 |
. . . . . . . . . 10
⊢
(∀𝑣 ∈
{𝑤 ∈ ℝ ∣
-𝑤 ∈ 𝐴}𝑣 ≤ 𝑢 ↔ ∀𝑣(𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → 𝑣 ≤ 𝑢)) |
45 | | df-ral 3068 |
. . . . . . . . . 10
⊢
(∀𝑣 ∈
ℝ (-𝑣 ∈ 𝐴 → 𝑣 ≤ 𝑢) ↔ ∀𝑣(𝑣 ∈ ℝ → (-𝑣 ∈ 𝐴 → 𝑣 ≤ 𝑢))) |
46 | 43, 44, 45 | 3bitr4ri 303 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
ℝ (-𝑣 ∈ 𝐴 → 𝑣 ≤ 𝑢) ↔ ∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 ≤ 𝑢) |
47 | | leneg 11408 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ ℝ ∧ 𝑢 ∈ ℝ) → (𝑣 ≤ 𝑢 ↔ -𝑢 ≤ -𝑣)) |
48 | 47 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑣 ≤ 𝑢 ↔ -𝑢 ≤ -𝑣)) |
49 | 48 | imbi2d 340 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → ((-𝑣 ∈ 𝐴 → 𝑣 ≤ 𝑢) ↔ (-𝑣 ∈ 𝐴 → -𝑢 ≤ -𝑣))) |
50 | 49 | ralbidva 3119 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℝ →
(∀𝑣 ∈ ℝ
(-𝑣 ∈ 𝐴 → 𝑣 ≤ 𝑢) ↔ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → -𝑢 ≤ -𝑣))) |
51 | 46, 50 | bitr3id 284 |
. . . . . . . 8
⊢ (𝑢 ∈ ℝ →
(∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 ≤ 𝑢 ↔ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → -𝑢 ≤ -𝑣))) |
52 | 51 | rexbiia 3176 |
. . . . . . 7
⊢
(∃𝑢 ∈
ℝ ∀𝑣 ∈
{𝑤 ∈ ℝ ∣
-𝑤 ∈ 𝐴}𝑣 ≤ 𝑢 ↔ ∃𝑢 ∈ ℝ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → -𝑢 ≤ -𝑣)) |
53 | 36, 52 | bitr4i 277 |
. . . . . 6
⊢
(∃𝑥 ∈
ℝ ∀𝑣 ∈
ℝ (-𝑣 ∈ 𝐴 → 𝑥 ≤ -𝑣) ↔ ∃𝑢 ∈ ℝ ∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 ≤ 𝑢) |
54 | 30, 53 | bitrdi 286 |
. . . . 5
⊢ (𝐴 ⊆ ℝ →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑢 ∈ ℝ ∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 ≤ 𝑢)) |
55 | 13, 54 | anbi12d 630 |
. . . 4
⊢ (𝐴 ⊆ ℝ → ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ↔ ({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ≠ ∅ ∧ ∃𝑢 ∈ ℝ ∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 ≤ 𝑢))) |
56 | | ssrab2 4009 |
. . . . 5
⊢ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ⊆ ℝ |
57 | | sup3 11862 |
. . . . 5
⊢ (({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ⊆ ℝ ∧ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ≠ ∅ ∧ ∃𝑢 ∈ ℝ ∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 ≤ 𝑢) → ∃𝑢 ∈ ℝ (∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑢 < 𝑣 ∧ ∀𝑣 ∈ ℝ (𝑣 < 𝑢 → ∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡))) |
58 | 56, 57 | mp3an1 1446 |
. . . 4
⊢ (({𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ≠ ∅ ∧ ∃𝑢 ∈ ℝ ∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 ≤ 𝑢) → ∃𝑢 ∈ ℝ (∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑢 < 𝑣 ∧ ∀𝑣 ∈ ℝ (𝑣 < 𝑢 → ∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡))) |
59 | 55, 58 | syl6bi 252 |
. . 3
⊢ (𝐴 ⊆ ℝ → ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑢 ∈ ℝ (∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑢 < 𝑣 ∧ ∀𝑣 ∈ ℝ (𝑣 < 𝑢 → ∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡)))) |
60 | 15 | imbi1d 341 |
. . . . . . . . 9
⊢ (𝐴 ⊆ ℝ → ((𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥) ↔ ((𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦 < 𝑥))) |
61 | | impexp 450 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦 < 𝑥) ↔ (𝑦 ∈ ℝ → (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥))) |
62 | 60, 61 | bitrdi 286 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ → ((𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥) ↔ (𝑦 ∈ ℝ → (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)))) |
63 | 62 | albidv 1924 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥) ↔ ∀𝑦(𝑦 ∈ ℝ → (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)))) |
64 | | df-ral 3068 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐴 ¬ 𝑦 < 𝑥 ↔ ∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) |
65 | | breq1 5073 |
. . . . . . . . . . 11
⊢ (𝑦 = -𝑣 → (𝑦 < 𝑥 ↔ -𝑣 < 𝑥)) |
66 | 65 | notbid 317 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑣 → (¬ 𝑦 < 𝑥 ↔ ¬ -𝑣 < 𝑥)) |
67 | 23, 66 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑦 = -𝑣 → ((𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥) ↔ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥))) |
68 | 21, 22, 67 | ralxfr 5332 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ℝ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥) ↔ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥)) |
69 | | df-ral 3068 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ℝ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥) ↔ ∀𝑦(𝑦 ∈ ℝ → (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥))) |
70 | 68, 69 | bitr3i 276 |
. . . . . . 7
⊢
(∀𝑣 ∈
ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥) ↔ ∀𝑦(𝑦 ∈ ℝ → (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥))) |
71 | 63, 64, 70 | 3bitr4g 313 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ↔ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥))) |
72 | | breq2 5074 |
. . . . . . . . 9
⊢ (𝑦 = -𝑣 → (𝑥 < 𝑦 ↔ 𝑥 < -𝑣)) |
73 | | breq2 5074 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑣 → (𝑧 < 𝑦 ↔ 𝑧 < -𝑣)) |
74 | 73 | rexbidv 3225 |
. . . . . . . . 9
⊢ (𝑦 = -𝑣 → (∃𝑧 ∈ 𝐴 𝑧 < 𝑦 ↔ ∃𝑧 ∈ 𝐴 𝑧 < -𝑣)) |
75 | 72, 74 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑦 = -𝑣 → ((𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ (𝑥 < -𝑣 → ∃𝑧 ∈ 𝐴 𝑧 < -𝑣))) |
76 | 21, 22, 75 | ralxfr 5332 |
. . . . . . 7
⊢
(∀𝑦 ∈
ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ ∀𝑣 ∈ ℝ (𝑥 < -𝑣 → ∃𝑧 ∈ 𝐴 𝑧 < -𝑣)) |
77 | | ssel 3910 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ ℝ → (𝑧 ∈ 𝐴 → 𝑧 ∈ ℝ)) |
78 | 77 | adantrd 491 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ ℝ → ((𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣) → 𝑧 ∈ ℝ)) |
79 | 78 | pm4.71rd 562 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ ℝ → ((𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣) ↔ (𝑧 ∈ ℝ ∧ (𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣)))) |
80 | 79 | exbidv 1925 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℝ →
(∃𝑧(𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣) ↔ ∃𝑧(𝑧 ∈ ℝ ∧ (𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣)))) |
81 | | df-rex 3069 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝐴 𝑧 < -𝑣 ↔ ∃𝑧(𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣)) |
82 | | renegcl 11214 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ → -𝑡 ∈
ℝ) |
83 | | infm3lem 11863 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ →
∃𝑡 ∈ ℝ
𝑧 = -𝑡) |
84 | | eleq1 2826 |
. . . . . . . . . . . . 13
⊢ (𝑧 = -𝑡 → (𝑧 ∈ 𝐴 ↔ -𝑡 ∈ 𝐴)) |
85 | | breq1 5073 |
. . . . . . . . . . . . 13
⊢ (𝑧 = -𝑡 → (𝑧 < -𝑣 ↔ -𝑡 < -𝑣)) |
86 | 84, 85 | anbi12d 630 |
. . . . . . . . . . . 12
⊢ (𝑧 = -𝑡 → ((𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣) ↔ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))) |
87 | 82, 83, 86 | rexxfr 5334 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
ℝ (𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣) ↔ ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)) |
88 | | df-rex 3069 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
ℝ (𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣) ↔ ∃𝑧(𝑧 ∈ ℝ ∧ (𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣))) |
89 | 87, 88 | bitr3i 276 |
. . . . . . . . . 10
⊢
(∃𝑡 ∈
ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣) ↔ ∃𝑧(𝑧 ∈ ℝ ∧ (𝑧 ∈ 𝐴 ∧ 𝑧 < -𝑣))) |
90 | 80, 81, 89 | 3bitr4g 313 |
. . . . . . . . 9
⊢ (𝐴 ⊆ ℝ →
(∃𝑧 ∈ 𝐴 𝑧 < -𝑣 ↔ ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))) |
91 | 90 | imbi2d 340 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ → ((𝑥 < -𝑣 → ∃𝑧 ∈ 𝐴 𝑧 < -𝑣) ↔ (𝑥 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)))) |
92 | 91 | ralbidv 3120 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(∀𝑣 ∈ ℝ
(𝑥 < -𝑣 → ∃𝑧 ∈ 𝐴 𝑧 < -𝑣) ↔ ∀𝑣 ∈ ℝ (𝑥 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)))) |
93 | 76, 92 | syl5bb 282 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
(∀𝑦 ∈ ℝ
(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ ∀𝑣 ∈ ℝ (𝑥 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)))) |
94 | 71, 93 | anbi12d 630 |
. . . . 5
⊢ (𝐴 ⊆ ℝ →
((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ (∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥) ∧ ∀𝑣 ∈ ℝ (𝑥 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))))) |
95 | 94 | rexbidv 3225 |
. . . 4
⊢ (𝐴 ⊆ ℝ →
(∃𝑥 ∈ ℝ
(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ ∃𝑥 ∈ ℝ (∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥) ∧ ∀𝑣 ∈ ℝ (𝑥 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))))) |
96 | | breq2 5074 |
. . . . . . . . . 10
⊢ (𝑥 = -𝑢 → (-𝑣 < 𝑥 ↔ -𝑣 < -𝑢)) |
97 | 96 | notbid 317 |
. . . . . . . . 9
⊢ (𝑥 = -𝑢 → (¬ -𝑣 < 𝑥 ↔ ¬ -𝑣 < -𝑢)) |
98 | 97 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑥 = -𝑢 → ((-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥) ↔ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < -𝑢))) |
99 | 98 | ralbidv 3120 |
. . . . . . 7
⊢ (𝑥 = -𝑢 → (∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥) ↔ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < -𝑢))) |
100 | | breq1 5073 |
. . . . . . . . 9
⊢ (𝑥 = -𝑢 → (𝑥 < -𝑣 ↔ -𝑢 < -𝑣)) |
101 | 100 | imbi1d 341 |
. . . . . . . 8
⊢ (𝑥 = -𝑢 → ((𝑥 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)) ↔ (-𝑢 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)))) |
102 | 101 | ralbidv 3120 |
. . . . . . 7
⊢ (𝑥 = -𝑢 → (∀𝑣 ∈ ℝ (𝑥 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)) ↔ ∀𝑣 ∈ ℝ (-𝑢 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)))) |
103 | 99, 102 | anbi12d 630 |
. . . . . 6
⊢ (𝑥 = -𝑢 → ((∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥) ∧ ∀𝑣 ∈ ℝ (𝑥 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))) ↔ (∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < -𝑢) ∧ ∀𝑣 ∈ ℝ (-𝑢 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))))) |
104 | 31, 32, 103 | rexxfr 5334 |
. . . . 5
⊢
(∃𝑥 ∈
ℝ (∀𝑣 ∈
ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥) ∧ ∀𝑣 ∈ ℝ (𝑥 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))) ↔ ∃𝑢 ∈ ℝ (∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < -𝑢) ∧ ∀𝑣 ∈ ℝ (-𝑢 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)))) |
105 | 39 | imbi1i 349 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → ¬ 𝑢 < 𝑣) ↔ ((𝑣 ∈ ℝ ∧ -𝑣 ∈ 𝐴) → ¬ 𝑢 < 𝑣)) |
106 | | impexp 450 |
. . . . . . . . . . 11
⊢ (((𝑣 ∈ ℝ ∧ -𝑣 ∈ 𝐴) → ¬ 𝑢 < 𝑣) ↔ (𝑣 ∈ ℝ → (-𝑣 ∈ 𝐴 → ¬ 𝑢 < 𝑣))) |
107 | 105, 106 | bitri 274 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → ¬ 𝑢 < 𝑣) ↔ (𝑣 ∈ ℝ → (-𝑣 ∈ 𝐴 → ¬ 𝑢 < 𝑣))) |
108 | 107 | albii 1823 |
. . . . . . . . 9
⊢
(∀𝑣(𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → ¬ 𝑢 < 𝑣) ↔ ∀𝑣(𝑣 ∈ ℝ → (-𝑣 ∈ 𝐴 → ¬ 𝑢 < 𝑣))) |
109 | | df-ral 3068 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
{𝑤 ∈ ℝ ∣
-𝑤 ∈ 𝐴} ¬ 𝑢 < 𝑣 ↔ ∀𝑣(𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → ¬ 𝑢 < 𝑣)) |
110 | | df-ral 3068 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
ℝ (-𝑣 ∈ 𝐴 → ¬ 𝑢 < 𝑣) ↔ ∀𝑣(𝑣 ∈ ℝ → (-𝑣 ∈ 𝐴 → ¬ 𝑢 < 𝑣))) |
111 | 108, 109,
110 | 3bitr4ri 303 |
. . . . . . . 8
⊢
(∀𝑣 ∈
ℝ (-𝑣 ∈ 𝐴 → ¬ 𝑢 < 𝑣) ↔ ∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑢 < 𝑣) |
112 | | ltneg 11405 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢 < 𝑣 ↔ -𝑣 < -𝑢)) |
113 | 112 | notbid 317 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (¬
𝑢 < 𝑣 ↔ ¬ -𝑣 < -𝑢)) |
114 | 113 | imbi2d 340 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → ((-𝑣 ∈ 𝐴 → ¬ 𝑢 < 𝑣) ↔ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < -𝑢))) |
115 | 114 | ralbidva 3119 |
. . . . . . . 8
⊢ (𝑢 ∈ ℝ →
(∀𝑣 ∈ ℝ
(-𝑣 ∈ 𝐴 → ¬ 𝑢 < 𝑣) ↔ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < -𝑢))) |
116 | 111, 115 | bitr3id 284 |
. . . . . . 7
⊢ (𝑢 ∈ ℝ →
(∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑢 < 𝑣 ↔ ∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < -𝑢))) |
117 | | ltneg 11405 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ ℝ ∧ 𝑢 ∈ ℝ) → (𝑣 < 𝑢 ↔ -𝑢 < -𝑣)) |
118 | 117 | ancoms 458 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑣 < 𝑢 ↔ -𝑢 < -𝑣)) |
119 | | negeq 11143 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑡 → -𝑤 = -𝑡) |
120 | 119 | eleq1d 2823 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑡 → (-𝑤 ∈ 𝐴 ↔ -𝑡 ∈ 𝐴)) |
121 | 120 | rexrab 3626 |
. . . . . . . . . . 11
⊢
(∃𝑡 ∈
{𝑤 ∈ ℝ ∣
-𝑤 ∈ 𝐴}𝑣 < 𝑡 ↔ ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ 𝑣 < 𝑡)) |
122 | | ltneg 11405 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑣 < 𝑡 ↔ -𝑡 < -𝑣)) |
123 | 122 | anbi2d 628 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ ℝ ∧ 𝑡 ∈ ℝ) → ((-𝑡 ∈ 𝐴 ∧ 𝑣 < 𝑡) ↔ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))) |
124 | 123 | rexbidva 3224 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ℝ →
(∃𝑡 ∈ ℝ
(-𝑡 ∈ 𝐴 ∧ 𝑣 < 𝑡) ↔ ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))) |
125 | 121, 124 | syl5bb 282 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ℝ →
(∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡 ↔ ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))) |
126 | 125 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) →
(∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡 ↔ ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))) |
127 | 118, 126 | imbi12d 344 |
. . . . . . . 8
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → ((𝑣 < 𝑢 → ∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡) ↔ (-𝑢 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)))) |
128 | 127 | ralbidva 3119 |
. . . . . . 7
⊢ (𝑢 ∈ ℝ →
(∀𝑣 ∈ ℝ
(𝑣 < 𝑢 → ∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡) ↔ ∀𝑣 ∈ ℝ (-𝑢 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)))) |
129 | 116, 128 | anbi12d 630 |
. . . . . 6
⊢ (𝑢 ∈ ℝ →
((∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑢 < 𝑣 ∧ ∀𝑣 ∈ ℝ (𝑣 < 𝑢 → ∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡)) ↔ (∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < -𝑢) ∧ ∀𝑣 ∈ ℝ (-𝑢 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))))) |
130 | 129 | rexbiia 3176 |
. . . . 5
⊢
(∃𝑢 ∈
ℝ (∀𝑣 ∈
{𝑤 ∈ ℝ ∣
-𝑤 ∈ 𝐴} ¬ 𝑢 < 𝑣 ∧ ∀𝑣 ∈ ℝ (𝑣 < 𝑢 → ∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡)) ↔ ∃𝑢 ∈ ℝ (∀𝑣 ∈ ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < -𝑢) ∧ ∀𝑣 ∈ ℝ (-𝑢 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣)))) |
131 | 104, 130 | bitr4i 277 |
. . . 4
⊢
(∃𝑥 ∈
ℝ (∀𝑣 ∈
ℝ (-𝑣 ∈ 𝐴 → ¬ -𝑣 < 𝑥) ∧ ∀𝑣 ∈ ℝ (𝑥 < -𝑣 → ∃𝑡 ∈ ℝ (-𝑡 ∈ 𝐴 ∧ -𝑡 < -𝑣))) ↔ ∃𝑢 ∈ ℝ (∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑢 < 𝑣 ∧ ∀𝑣 ∈ ℝ (𝑣 < 𝑢 → ∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡))) |
132 | 95, 131 | bitrdi 286 |
. . 3
⊢ (𝐴 ⊆ ℝ →
(∃𝑥 ∈ ℝ
(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ ∃𝑢 ∈ ℝ (∀𝑣 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑢 < 𝑣 ∧ ∀𝑣 ∈ ℝ (𝑣 < 𝑢 → ∃𝑡 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑣 < 𝑡)))) |
133 | 59, 132 | sylibrd 258 |
. 2
⊢ (𝐴 ⊆ ℝ → ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
134 | 133 | 3impib 1114 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |