Step | Hyp | Ref
| Expression |
1 | | dedekindeu.lss |
. . 3
⊢ (𝜑 → 𝐿 ⊆ ℝ) |
2 | | dedekindeu.uss |
. . 3
⊢ (𝜑 → 𝑈 ⊆ ℝ) |
3 | | dedekindeu.lm |
. . 3
⊢ (𝜑 → ∃𝑞 ∈ ℝ 𝑞 ∈ 𝐿) |
4 | | dedekindeu.um |
. . 3
⊢ (𝜑 → ∃𝑟 ∈ ℝ 𝑟 ∈ 𝑈) |
5 | | dedekindeu.lr |
. . 3
⊢ (𝜑 → ∀𝑞 ∈ ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)) |
6 | | dedekindeu.ur |
. . 3
⊢ (𝜑 → ∀𝑟 ∈ ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)) |
7 | | dedekindeu.disj |
. . 3
⊢ (𝜑 → (𝐿 ∩ 𝑈) = ∅) |
8 | | dedekindeu.loc |
. . 3
⊢ (𝜑 → ∀𝑞 ∈ ℝ ∀𝑟 ∈ ℝ (𝑞 < 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | dedekindeulemlub 13351 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) |
10 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 ∈ 𝐿) |
11 | 1 | ad3antrrr 489 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝐿 ⊆ ℝ) |
12 | 11, 10 | sseldd 3148 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 ∈ ℝ) |
13 | | rsp 2517 |
. . . . . . . . . . 11
⊢
(∀𝑞 ∈
ℝ (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟) → (𝑞 ∈ ℝ → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))) |
14 | 5, 13 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑞 ∈ ℝ → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))) |
15 | 14 | ad3antrrr 489 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → (𝑞 ∈ ℝ → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟))) |
16 | 12, 15 | mpd 13 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)) |
17 | 10, 16 | mpbid 146 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → ∃𝑟 ∈ 𝐿 𝑞 < 𝑟) |
18 | 12 | adantr 274 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ ℝ) |
19 | 11 | adantr 274 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝐿 ⊆ ℝ) |
20 | | simprl 526 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ 𝐿) |
21 | 19, 20 | sseldd 3148 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ ℝ) |
22 | | simp-4r 537 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ ℝ) |
23 | | simprr 527 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑟) |
24 | | breq2 3991 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑟 → (𝑥 < 𝑦 ↔ 𝑥 < 𝑟)) |
25 | 24 | notbid 662 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑟 → (¬ 𝑥 < 𝑦 ↔ ¬ 𝑥 < 𝑟)) |
26 | | simprl 526 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦) |
27 | 26 | ad2antrr 485 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → ∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦) |
28 | 25, 27, 20 | rspcdva 2839 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → ¬ 𝑥 < 𝑟) |
29 | 21, 22, 28 | nltled 8027 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑟 ≤ 𝑥) |
30 | 18, 21, 22, 23, 29 | ltletrd 8329 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) ∧ (𝑟 ∈ 𝐿 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑥) |
31 | 17, 30 | rexlimddv 2592 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑞 ∈ 𝐿) → 𝑞 < 𝑥) |
32 | 31 | ralrimiva 2543 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑞 ∈ 𝐿 𝑞 < 𝑥) |
33 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑟 ∈ 𝑈) |
34 | | simplll 528 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝜑) |
35 | 34, 2 | syl 14 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑈 ⊆ ℝ) |
36 | 35, 33 | sseldd 3148 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑟 ∈ ℝ) |
37 | | rsp 2517 |
. . . . . . . . . 10
⊢
(∀𝑟 ∈
ℝ (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟) → (𝑟 ∈ ℝ → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))) |
38 | 6, 37 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → (𝑟 ∈ ℝ → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟))) |
39 | 34, 36, 38 | sylc 62 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ 𝑈 𝑞 < 𝑟)) |
40 | 33, 39 | mpbid 146 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → ∃𝑞 ∈ 𝑈 𝑞 < 𝑟) |
41 | | simp-4r 537 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ∈ ℝ) |
42 | 35 | adantr 274 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑈 ⊆ ℝ) |
43 | | simprl 526 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ 𝑈) |
44 | 42, 43 | sseldd 3148 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 ∈ ℝ) |
45 | 36 | adantr 274 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑟 ∈ ℝ) |
46 | 43 | adantr 274 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ 𝑈) |
47 | 34 | ad2antrr 485 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝜑) |
48 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 < 𝑥) |
49 | | breq1 3990 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑞 → (𝑦 < 𝑥 ↔ 𝑞 < 𝑥)) |
50 | | breq1 3990 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑞 → (𝑦 < 𝑧 ↔ 𝑞 < 𝑧)) |
51 | 50 | rexbidv 2471 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑞 → (∃𝑧 ∈ 𝐿 𝑦 < 𝑧 ↔ ∃𝑧 ∈ 𝐿 𝑞 < 𝑧)) |
52 | 49, 51 | imbi12d 233 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑞 → ((𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧) ↔ (𝑞 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧))) |
53 | | simprr 527 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)) |
54 | 53 | ad3antrrr 489 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)) |
55 | 44 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ ℝ) |
56 | 52, 54, 55 | rspcdva 2839 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧)) |
57 | 48, 56 | mpd 13 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑧 ∈ 𝐿 𝑞 < 𝑧) |
58 | | breq2 3991 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑟 → (𝑞 < 𝑧 ↔ 𝑞 < 𝑟)) |
59 | 58 | cbvrexv 2697 |
. . . . . . . . . . . . 13
⊢
(∃𝑧 ∈
𝐿 𝑞 < 𝑧 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟) |
60 | 57, 59 | sylib 121 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ∃𝑟 ∈ 𝐿 𝑞 < 𝑟) |
61 | 47, 55, 14 | sylc 62 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ 𝐿 𝑞 < 𝑟)) |
62 | 60, 61 | mpbird 166 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → 𝑞 ∈ 𝐿) |
63 | | disj 3462 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∩ 𝑈) = ∅ ↔ ∀𝑞 ∈ 𝐿 ¬ 𝑞 ∈ 𝑈) |
64 | 7, 63 | sylib 121 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑞 ∈ 𝐿 ¬ 𝑞 ∈ 𝑈) |
65 | 64 | r19.21bi 2558 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐿) → ¬ 𝑞 ∈ 𝑈) |
66 | 47, 62, 65 | syl2anc 409 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) ∧ 𝑞 < 𝑥) → ¬ 𝑞 ∈ 𝑈) |
67 | 46, 66 | pm2.65da 656 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → ¬ 𝑞 < 𝑥) |
68 | 41, 44, 67 | nltled 8027 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 ≤ 𝑞) |
69 | | simprr 527 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑞 < 𝑟) |
70 | 41, 44, 45, 68, 69 | lelttrd 8031 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) ∧ (𝑞 ∈ 𝑈 ∧ 𝑞 < 𝑟)) → 𝑥 < 𝑟) |
71 | 40, 70 | rexlimddv 2592 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) ∧ 𝑟 ∈ 𝑈) → 𝑥 < 𝑟) |
72 | 71 | ralrimiva 2543 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → ∀𝑟 ∈ 𝑈 𝑥 < 𝑟) |
73 | 32, 72 | jca 304 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧))) → (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)) |
74 | 73 | ex 114 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)) → (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))) |
75 | 74 | reximdva 2572 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐿 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐿 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟))) |
76 | 9, 75 | mpd 13 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑞 ∈ 𝐿 𝑞 < 𝑥 ∧ ∀𝑟 ∈ 𝑈 𝑥 < 𝑟)) |