Step | Hyp | Ref
| Expression |
1 | | supinfneg.ex |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
2 | | breq1 3990 |
. . . . . . . 8
⊢ (𝑎 = 𝑥 → (𝑎 < 𝑦 ↔ 𝑥 < 𝑦)) |
3 | 2 | notbid 662 |
. . . . . . 7
⊢ (𝑎 = 𝑥 → (¬ 𝑎 < 𝑦 ↔ ¬ 𝑥 < 𝑦)) |
4 | 3 | ralbidv 2470 |
. . . . . 6
⊢ (𝑎 = 𝑥 → (∀𝑦 ∈ 𝐴 ¬ 𝑎 < 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦)) |
5 | | breq2 3991 |
. . . . . . . 8
⊢ (𝑎 = 𝑥 → (𝑦 < 𝑎 ↔ 𝑦 < 𝑥)) |
6 | 5 | imbi1d 230 |
. . . . . . 7
⊢ (𝑎 = 𝑥 → ((𝑦 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ↔ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
7 | 6 | ralbidv 2470 |
. . . . . 6
⊢ (𝑎 = 𝑥 → (∀𝑦 ∈ ℝ (𝑦 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
8 | 4, 7 | anbi12d 470 |
. . . . 5
⊢ (𝑎 = 𝑥 → ((∀𝑦 ∈ 𝐴 ¬ 𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))) |
9 | 8 | cbvrexv 2697 |
. . . 4
⊢
(∃𝑎 ∈
ℝ (∀𝑦 ∈
𝐴 ¬ 𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
10 | 1, 9 | sylibr 133 |
. . 3
⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
11 | | breq2 3991 |
. . . . . . 7
⊢ (𝑏 = 𝑦 → (𝑎 < 𝑏 ↔ 𝑎 < 𝑦)) |
12 | 11 | notbid 662 |
. . . . . 6
⊢ (𝑏 = 𝑦 → (¬ 𝑎 < 𝑏 ↔ ¬ 𝑎 < 𝑦)) |
13 | 12 | cbvralv 2696 |
. . . . 5
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑎 < 𝑏 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑎 < 𝑦) |
14 | | breq2 3991 |
. . . . . . . . 9
⊢ (𝑐 = 𝑧 → (𝑏 < 𝑐 ↔ 𝑏 < 𝑧)) |
15 | 14 | cbvrexv 2697 |
. . . . . . . 8
⊢
(∃𝑐 ∈
𝐴 𝑏 < 𝑐 ↔ ∃𝑧 ∈ 𝐴 𝑏 < 𝑧) |
16 | 15 | imbi2i 225 |
. . . . . . 7
⊢ ((𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐) ↔ (𝑏 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑏 < 𝑧)) |
17 | 16 | ralbii 2476 |
. . . . . 6
⊢
(∀𝑏 ∈
ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐) ↔ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑏 < 𝑧)) |
18 | | breq1 3990 |
. . . . . . . 8
⊢ (𝑏 = 𝑦 → (𝑏 < 𝑎 ↔ 𝑦 < 𝑎)) |
19 | | breq1 3990 |
. . . . . . . . 9
⊢ (𝑏 = 𝑦 → (𝑏 < 𝑧 ↔ 𝑦 < 𝑧)) |
20 | 19 | rexbidv 2471 |
. . . . . . . 8
⊢ (𝑏 = 𝑦 → (∃𝑧 ∈ 𝐴 𝑏 < 𝑧 ↔ ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) |
21 | 18, 20 | imbi12d 233 |
. . . . . . 7
⊢ (𝑏 = 𝑦 → ((𝑏 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑏 < 𝑧) ↔ (𝑦 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
22 | 21 | cbvralv 2696 |
. . . . . 6
⊢
(∀𝑏 ∈
ℝ (𝑏 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑏 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) |
23 | 17, 22 | bitri 183 |
. . . . 5
⊢
(∀𝑏 ∈
ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐) ↔ ∀𝑦 ∈ ℝ (𝑦 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) |
24 | 13, 23 | anbi12i 457 |
. . . 4
⊢
((∀𝑏 ∈
𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
25 | 24 | rexbii 2477 |
. . 3
⊢
(∃𝑎 ∈
ℝ (∀𝑏 ∈
𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ↔ ∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑎 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
26 | 10, 25 | sylibr 133 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐))) |
27 | | renegcl 8167 |
. . . . . 6
⊢ (𝑎 ∈ ℝ → -𝑎 ∈
ℝ) |
28 | 27 | ad2antlr 486 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐))) → -𝑎 ∈ ℝ) |
29 | | simplr 525 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐))) → 𝑎 ∈ ℝ) |
30 | | simprl 526 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐))) → ∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏) |
31 | | elrabi 2883 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → 𝑦 ∈ ℝ) |
32 | | negeq 8099 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑦 → -𝑤 = -𝑦) |
33 | 32 | eleq1d 2239 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑦 → (-𝑤 ∈ 𝐴 ↔ -𝑦 ∈ 𝐴)) |
34 | 33 | elrab3 2887 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ -𝑦 ∈ 𝐴)) |
35 | 34 | biimpd 143 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → -𝑦 ∈ 𝐴)) |
36 | 31, 35 | mpcom 36 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → -𝑦 ∈ 𝐴) |
37 | | breq2 3991 |
. . . . . . . . . . . . 13
⊢ (𝑏 = -𝑦 → (𝑎 < 𝑏 ↔ 𝑎 < -𝑦)) |
38 | 37 | notbid 662 |
. . . . . . . . . . . 12
⊢ (𝑏 = -𝑦 → (¬ 𝑎 < 𝑏 ↔ ¬ 𝑎 < -𝑦)) |
39 | 38 | rspcv 2830 |
. . . . . . . . . . 11
⊢ (-𝑦 ∈ 𝐴 → (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 → ¬ 𝑎 < -𝑦)) |
40 | 36, 39 | syl 14 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 → ¬ 𝑎 < -𝑦)) |
41 | 40 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 → ¬ 𝑎 < -𝑦)) |
42 | | ltnegcon2 8370 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦)) |
43 | 42 | notbid 662 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (¬
𝑦 < -𝑎 ↔ ¬ 𝑎 < -𝑦)) |
44 | 31, 43 | sylan 281 |
. . . . . . . . 9
⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (¬ 𝑦 < -𝑎 ↔ ¬ 𝑎 < -𝑦)) |
45 | 41, 44 | sylibrd 168 |
. . . . . . . 8
⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 → ¬ 𝑦 < -𝑎)) |
46 | 45 | ancoms 266 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}) → (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 → ¬ 𝑦 < -𝑎)) |
47 | 46 | ralrimdva 2550 |
. . . . . 6
⊢ (𝑎 ∈ ℝ →
(∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 → ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < -𝑎)) |
48 | 29, 30, 47 | sylc 62 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐))) → ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < -𝑎) |
49 | | nfv 1521 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑐(𝜑 ∧ 𝑎 ∈ ℝ) |
50 | | nfcv 2312 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑐ℝ |
51 | | nfv 1521 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑐 𝑏 < 𝑎 |
52 | | nfre1 2513 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑐∃𝑐 ∈ 𝐴 𝑏 < 𝑐 |
53 | 51, 52 | nfim 1565 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑐(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐) |
54 | 50, 53 | nfralya 2510 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑐∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐) |
55 | 49, 54 | nfan 1558 |
. . . . . . . . . . 11
⊢
Ⅎ𝑐((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) |
56 | | nfv 1521 |
. . . . . . . . . . 11
⊢
Ⅎ𝑐 𝑦 ∈ ℝ |
57 | 55, 56 | nfan 1558 |
. . . . . . . . . 10
⊢
Ⅎ𝑐(((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) |
58 | | nfv 1521 |
. . . . . . . . . 10
⊢
Ⅎ𝑐-𝑎 < 𝑦 |
59 | 57, 58 | nfan 1558 |
. . . . . . . . 9
⊢
Ⅎ𝑐((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) |
60 | | simplr 525 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → 𝑐 ∈ 𝐴) |
61 | | supinfneg.ss |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
62 | 61 | sseld 3146 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑐 ∈ 𝐴 → 𝑐 ∈ ℝ)) |
63 | 62 | ad6antr 495 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → (𝑐 ∈ 𝐴 → 𝑐 ∈ ℝ)) |
64 | 60, 63 | mpd 13 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → 𝑐 ∈ ℝ) |
65 | 64 | renegcld 8286 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → -𝑐 ∈ ℝ) |
66 | 64 | recnd 7935 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → 𝑐 ∈ ℂ) |
67 | 66 | negnegd 8208 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → --𝑐 = 𝑐) |
68 | 67, 60 | eqeltrd 2247 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → --𝑐 ∈ 𝐴) |
69 | | negeq 8099 |
. . . . . . . . . . . . 13
⊢ (𝑤 = -𝑐 → -𝑤 = --𝑐) |
70 | 69 | eleq1d 2239 |
. . . . . . . . . . . 12
⊢ (𝑤 = -𝑐 → (-𝑤 ∈ 𝐴 ↔ --𝑐 ∈ 𝐴)) |
71 | 70 | elrab 2886 |
. . . . . . . . . . 11
⊢ (-𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ (-𝑐 ∈ ℝ ∧ --𝑐 ∈ 𝐴)) |
72 | 65, 68, 71 | sylanbrc 415 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → -𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}) |
73 | | simp-4r 537 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → 𝑦 ∈ ℝ) |
74 | | simpr 109 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → -𝑦 < 𝑐) |
75 | 73, 64, 74 | ltnegcon1d 8431 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → -𝑐 < 𝑦) |
76 | | breq1 3990 |
. . . . . . . . . . 11
⊢ (𝑧 = -𝑐 → (𝑧 < 𝑦 ↔ -𝑐 < 𝑦)) |
77 | 76 | rspcev 2834 |
. . . . . . . . . 10
⊢ ((-𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ -𝑐 < 𝑦) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦) |
78 | 72, 75, 77 | syl2anc 409 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) ∧ 𝑐 ∈ 𝐴) ∧ -𝑦 < 𝑐) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦) |
79 | | simpllr 529 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) → 𝑎 ∈ ℝ) |
80 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
81 | | simplr 525 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) → ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) |
82 | 79, 80, 81 | jca31 307 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) → ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐))) |
83 | | ltnegcon1 8369 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-𝑎 < 𝑦 ↔ -𝑦 < 𝑎)) |
84 | 83 | adantr 274 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) → (-𝑎 < 𝑦 ↔ -𝑦 < 𝑎)) |
85 | | renegcl 8167 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ → -𝑦 ∈
ℝ) |
86 | | breq1 3990 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = -𝑦 → (𝑏 < 𝑎 ↔ -𝑦 < 𝑎)) |
87 | | breq1 3990 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = -𝑦 → (𝑏 < 𝑐 ↔ -𝑦 < 𝑐)) |
88 | 87 | rexbidv 2471 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = -𝑦 → (∃𝑐 ∈ 𝐴 𝑏 < 𝑐 ↔ ∃𝑐 ∈ 𝐴 -𝑦 < 𝑐)) |
89 | 86, 88 | imbi12d 233 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = -𝑦 → ((𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐) ↔ (-𝑦 < 𝑎 → ∃𝑐 ∈ 𝐴 -𝑦 < 𝑐))) |
90 | 89 | rspcv 2830 |
. . . . . . . . . . . . . . 15
⊢ (-𝑦 ∈ ℝ →
(∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐) → (-𝑦 < 𝑎 → ∃𝑐 ∈ 𝐴 -𝑦 < 𝑐))) |
91 | 85, 90 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ →
(∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐) → (-𝑦 < 𝑎 → ∃𝑐 ∈ 𝐴 -𝑦 < 𝑐))) |
92 | 91 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐) → (-𝑦 < 𝑎 → ∃𝑐 ∈ 𝐴 -𝑦 < 𝑐))) |
93 | 92 | imp 123 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) → (-𝑦 < 𝑎 → ∃𝑐 ∈ 𝐴 -𝑦 < 𝑐)) |
94 | 84, 93 | sylbid 149 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) → (-𝑎 < 𝑦 → ∃𝑐 ∈ 𝐴 -𝑦 < 𝑐)) |
95 | 94 | imp 123 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ -𝑎 < 𝑦) → ∃𝑐 ∈ 𝐴 -𝑦 < 𝑐) |
96 | 82, 95 | sylan 281 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) → ∃𝑐 ∈ 𝐴 -𝑦 < 𝑐) |
97 | 59, 78, 96 | r19.29af 2611 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ ℝ) ∧
∀𝑏 ∈ ℝ
(𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) ∧ -𝑎 < 𝑦) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦) |
98 | 97 | ex 114 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) ∧ 𝑦 ∈ ℝ) → (-𝑎 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦)) |
99 | 98 | ralrimiva 2543 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) → ∀𝑦 ∈ ℝ (-𝑎 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦)) |
100 | 99 | adantrl 475 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐))) → ∀𝑦 ∈ ℝ (-𝑎 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦)) |
101 | | breq2 3991 |
. . . . . . . . 9
⊢ (𝑥 = -𝑎 → (𝑦 < 𝑥 ↔ 𝑦 < -𝑎)) |
102 | 101 | notbid 662 |
. . . . . . . 8
⊢ (𝑥 = -𝑎 → (¬ 𝑦 < 𝑥 ↔ ¬ 𝑦 < -𝑎)) |
103 | 102 | ralbidv 2470 |
. . . . . . 7
⊢ (𝑥 = -𝑎 → (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ↔ ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < -𝑎)) |
104 | | breq1 3990 |
. . . . . . . . 9
⊢ (𝑥 = -𝑎 → (𝑥 < 𝑦 ↔ -𝑎 < 𝑦)) |
105 | 104 | imbi1d 230 |
. . . . . . . 8
⊢ (𝑥 = -𝑎 → ((𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦) ↔ (-𝑎 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦))) |
106 | 105 | ralbidv 2470 |
. . . . . . 7
⊢ (𝑥 = -𝑎 → (∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦) ↔ ∀𝑦 ∈ ℝ (-𝑎 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦))) |
107 | 103, 106 | anbi12d 470 |
. . . . . 6
⊢ (𝑥 = -𝑎 → ((∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦)) ↔ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < -𝑎 ∧ ∀𝑦 ∈ ℝ (-𝑎 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦)))) |
108 | 107 | rspcev 2834 |
. . . . 5
⊢ ((-𝑎 ∈ ℝ ∧
(∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < -𝑎 ∧ ∀𝑦 ∈ ℝ (-𝑎 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦))) |
109 | 28, 48, 100, 108 | syl12anc 1231 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦))) |
110 | 109 | ex 114 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ((∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦)))) |
111 | 110 | rexlimdva 2587 |
. 2
⊢ (𝜑 → (∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ ℝ (𝑏 < 𝑎 → ∃𝑐 ∈ 𝐴 𝑏 < 𝑐)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦)))) |
112 | 26, 111 | mpd 13 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑧 < 𝑦))) |