Step | Hyp | Ref
| Expression |
1 | | axpre-suploclem.ss |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
2 | | axpre-suploclem.m |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
3 | 1, 2 | sseldd 3129 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) |
4 | | elreal2 7752 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ ↔
((1st ‘𝐶)
∈ R ∧ 𝐶 = 〈(1st ‘𝐶),
0R〉)) |
5 | 3, 4 | sylib 121 |
. . . . . 6
⊢ (𝜑 → ((1st
‘𝐶) ∈
R ∧ 𝐶 =
〈(1st ‘𝐶),
0R〉)) |
6 | 5 | simpld 111 |
. . . . 5
⊢ (𝜑 → (1st
‘𝐶) ∈
R) |
7 | 5 | simprd 113 |
. . . . . 6
⊢ (𝜑 → 𝐶 = 〈(1st ‘𝐶),
0R〉) |
8 | 7, 2 | eqeltrrd 2235 |
. . . . 5
⊢ (𝜑 → 〈(1st
‘𝐶),
0R〉 ∈ 𝐴) |
9 | | opeq1 3743 |
. . . . . . 7
⊢ (𝑤 = (1st ‘𝐶) → 〈𝑤,
0R〉 = 〈(1st ‘𝐶),
0R〉) |
10 | 9 | eleq1d 2226 |
. . . . . 6
⊢ (𝑤 = (1st ‘𝐶) → (〈𝑤,
0R〉 ∈ 𝐴 ↔ 〈(1st ‘𝐶),
0R〉 ∈ 𝐴)) |
11 | | axpre-suploclem.b |
. . . . . 6
⊢ 𝐵 = {𝑤 ∈ R ∣ 〈𝑤,
0R〉 ∈ 𝐴} |
12 | 10, 11 | elrab2 2871 |
. . . . 5
⊢
((1st ‘𝐶) ∈ 𝐵 ↔ ((1st ‘𝐶) ∈ R ∧
〈(1st ‘𝐶), 0R〉 ∈
𝐴)) |
13 | 6, 8, 12 | sylanbrc 414 |
. . . 4
⊢ (𝜑 → (1st
‘𝐶) ∈ 𝐵) |
14 | | eleq1 2220 |
. . . . 5
⊢ (𝑎 = (1st ‘𝐶) → (𝑎 ∈ 𝐵 ↔ (1st ‘𝐶) ∈ 𝐵)) |
15 | 14 | spcegv 2800 |
. . . 4
⊢
((1st ‘𝐶) ∈ 𝐵 → ((1st ‘𝐶) ∈ 𝐵 → ∃𝑎 𝑎 ∈ 𝐵)) |
16 | 13, 13, 15 | sylc 62 |
. . 3
⊢ (𝜑 → ∃𝑎 𝑎 ∈ 𝐵) |
17 | | axpre-suploclem.ub |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) |
18 | | simprl 521 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → 𝑥 ∈ ℝ) |
19 | | elreal2 7752 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↔
((1st ‘𝑥)
∈ R ∧ 𝑥 = 〈(1st ‘𝑥),
0R〉)) |
20 | 18, 19 | sylib 121 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → ((1st ‘𝑥) ∈ R ∧
𝑥 = 〈(1st
‘𝑥),
0R〉)) |
21 | 20 | simpld 111 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → (1st ‘𝑥) ∈
R) |
22 | | breq1 3970 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑏, 0R〉 →
(𝑦 <ℝ
𝑥 ↔ 〈𝑏,
0R〉 <ℝ 𝑥)) |
23 | | simplrr 526 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) ∧ 𝑏 ∈ 𝐵) → ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) |
24 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
25 | | opeq1 3743 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑏 → 〈𝑤, 0R〉 =
〈𝑏,
0R〉) |
26 | 25 | eleq1d 2226 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑏 → (〈𝑤, 0R〉 ∈
𝐴 ↔ 〈𝑏,
0R〉 ∈ 𝐴)) |
27 | 26, 11 | elrab2 2871 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ R ∧ 〈𝑏,
0R〉 ∈ 𝐴)) |
28 | 24, 27 | sylib 121 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) ∧ 𝑏 ∈ 𝐵) → (𝑏 ∈ R ∧ 〈𝑏,
0R〉 ∈ 𝐴)) |
29 | 28 | simprd 113 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) ∧ 𝑏 ∈ 𝐵) → 〈𝑏, 0R〉 ∈
𝐴) |
30 | 22, 23, 29 | rspcdva 2821 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) ∧ 𝑏 ∈ 𝐵) → 〈𝑏, 0R〉
<ℝ 𝑥) |
31 | | simplrl 525 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) ∧ 𝑏 ∈ 𝐵) → 𝑥 ∈ ℝ) |
32 | 31, 19 | sylib 121 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) ∧ 𝑏 ∈ 𝐵) → ((1st ‘𝑥) ∈ R ∧
𝑥 = 〈(1st
‘𝑥),
0R〉)) |
33 | 32 | simprd 113 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) ∧ 𝑏 ∈ 𝐵) → 𝑥 = 〈(1st ‘𝑥),
0R〉) |
34 | 30, 33 | breqtrd 3992 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) ∧ 𝑏 ∈ 𝐵) → 〈𝑏, 0R〉
<ℝ 〈(1st ‘𝑥),
0R〉) |
35 | | ltresr 7761 |
. . . . . . 7
⊢
(〈𝑏,
0R〉 <ℝ 〈(1st
‘𝑥),
0R〉 ↔ 𝑏 <R
(1st ‘𝑥)) |
36 | 34, 35 | sylib 121 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) ∧ 𝑏 ∈ 𝐵) → 𝑏 <R
(1st ‘𝑥)) |
37 | 36 | ralrimiva 2530 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → ∀𝑏 ∈ 𝐵 𝑏 <R
(1st ‘𝑥)) |
38 | | brralrspcev 4024 |
. . . . 5
⊢
(((1st ‘𝑥) ∈ R ∧ ∀𝑏 ∈ 𝐵 𝑏 <R
(1st ‘𝑥))
→ ∃𝑎 ∈
R ∀𝑏
∈ 𝐵 𝑏 <R 𝑎) |
39 | 21, 37, 38 | syl2anc 409 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → ∃𝑎 ∈ R ∀𝑏 ∈ 𝐵 𝑏 <R 𝑎) |
40 | 17, 39 | rexlimddv 2579 |
. . 3
⊢ (𝜑 → ∃𝑎 ∈ R ∀𝑏 ∈ 𝐵 𝑏 <R 𝑎) |
41 | | simpr 109 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → 𝑎 <R 𝑏) |
42 | | ltresr 7761 |
. . . . . . . 8
⊢
(〈𝑎,
0R〉 <ℝ 〈𝑏,
0R〉 ↔ 𝑎 <R 𝑏) |
43 | 41, 42 | sylibr 133 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → 〈𝑎, 0R〉
<ℝ 〈𝑏,
0R〉) |
44 | | breq2 3971 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑏, 0R〉 →
(〈𝑎,
0R〉 <ℝ 𝑦 ↔ 〈𝑎, 0R〉
<ℝ 〈𝑏,
0R〉)) |
45 | | breq2 3971 |
. . . . . . . . . . 11
⊢ (𝑦 = 〈𝑏, 0R〉 →
(𝑧 <ℝ
𝑦 ↔ 𝑧 <ℝ 〈𝑏,
0R〉)) |
46 | 45 | ralbidv 2457 |
. . . . . . . . . 10
⊢ (𝑦 = 〈𝑏, 0R〉 →
(∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦 ↔ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉)) |
47 | 46 | orbi2d 780 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑏, 0R〉 →
((∃𝑧 ∈ 𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦) ↔ (∃𝑧 ∈ 𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉))) |
48 | 44, 47 | imbi12d 233 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑏, 0R〉 →
((〈𝑎,
0R〉 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)) ↔ (〈𝑎, 0R〉
<ℝ 〈𝑏, 0R〉 →
(∃𝑧 ∈ 𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉)))) |
49 | | breq1 3970 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑎, 0R〉 →
(𝑥 <ℝ
𝑦 ↔ 〈𝑎,
0R〉 <ℝ 𝑦)) |
50 | | breq1 3970 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝑎, 0R〉 →
(𝑥 <ℝ
𝑧 ↔ 〈𝑎,
0R〉 <ℝ 𝑧)) |
51 | 50 | rexbidv 2458 |
. . . . . . . . . . . 12
⊢ (𝑥 = 〈𝑎, 0R〉 →
(∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ↔ ∃𝑧 ∈ 𝐴 〈𝑎, 0R〉
<ℝ 𝑧)) |
52 | 51 | orbi1d 781 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑎, 0R〉 →
((∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦) ↔ (∃𝑧 ∈ 𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦))) |
53 | 49, 52 | imbi12d 233 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑎, 0R〉 →
((𝑥 <ℝ
𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)) ↔ (〈𝑎, 0R〉
<ℝ 𝑦
→ (∃𝑧 ∈
𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) |
54 | 53 | ralbidv 2457 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑎, 0R〉 →
(∀𝑦 ∈ ℝ
(𝑥 <ℝ
𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)) ↔ ∀𝑦 ∈ ℝ (〈𝑎, 0R〉
<ℝ 𝑦
→ (∃𝑧 ∈
𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) |
55 | | axpre-suploclem.loc |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦))) |
56 | 55 | ad2antrr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦))) |
57 | | simplrl 525 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → 𝑎 ∈ R) |
58 | | opelreal 7749 |
. . . . . . . . . 10
⊢
(〈𝑎,
0R〉 ∈ ℝ ↔ 𝑎 ∈ R) |
59 | 57, 58 | sylibr 133 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → 〈𝑎, 0R〉 ∈
ℝ) |
60 | 54, 56, 59 | rspcdva 2821 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → ∀𝑦 ∈ ℝ (〈𝑎, 0R〉
<ℝ 𝑦
→ (∃𝑧 ∈
𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦))) |
61 | | simplrr 526 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → 𝑏 ∈ R) |
62 | | opelreal 7749 |
. . . . . . . . 9
⊢
(〈𝑏,
0R〉 ∈ ℝ ↔ 𝑏 ∈ R) |
63 | 61, 62 | sylibr 133 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → 〈𝑏, 0R〉 ∈
ℝ) |
64 | 48, 60, 63 | rspcdva 2821 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → (〈𝑎, 0R〉
<ℝ 〈𝑏, 0R〉 →
(∃𝑧 ∈ 𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉))) |
65 | 43, 64 | mpd 13 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → (∃𝑧 ∈ 𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉)) |
66 | | simplll 523 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ 𝜑) |
67 | | simprl 521 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ 𝑧 ∈ 𝐴) |
68 | 1 | sseld 3127 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑧 ∈ 𝐴 → 𝑧 ∈ ℝ)) |
69 | 66, 67, 68 | sylc 62 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ 𝑧 ∈
ℝ) |
70 | | elreal2 7752 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ ↔
((1st ‘𝑧)
∈ R ∧ 𝑧 = 〈(1st ‘𝑧),
0R〉)) |
71 | 69, 70 | sylib 121 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ ((1st ‘𝑧) ∈ R ∧ 𝑧 = 〈(1st
‘𝑧),
0R〉)) |
72 | 71 | simpld 111 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ (1st ‘𝑧) ∈ R) |
73 | 71 | simprd 113 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ 𝑧 =
〈(1st ‘𝑧),
0R〉) |
74 | 73, 67 | eqeltrrd 2235 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ 〈(1st ‘𝑧), 0R〉 ∈
𝐴) |
75 | | opeq1 3743 |
. . . . . . . . . . . 12
⊢ (𝑤 = (1st ‘𝑧) → 〈𝑤,
0R〉 = 〈(1st ‘𝑧),
0R〉) |
76 | 75 | eleq1d 2226 |
. . . . . . . . . . 11
⊢ (𝑤 = (1st ‘𝑧) → (〈𝑤,
0R〉 ∈ 𝐴 ↔ 〈(1st ‘𝑧),
0R〉 ∈ 𝐴)) |
77 | 76, 11 | elrab2 2871 |
. . . . . . . . . 10
⊢
((1st ‘𝑧) ∈ 𝐵 ↔ ((1st ‘𝑧) ∈ R ∧
〈(1st ‘𝑧), 0R〉 ∈
𝐴)) |
78 | 72, 74, 77 | sylanbrc 414 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ (1st ‘𝑧) ∈ 𝐵) |
79 | | simprr 522 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ 〈𝑎,
0R〉 <ℝ 𝑧) |
80 | 79, 73 | breqtrd 3992 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ 〈𝑎,
0R〉 <ℝ 〈(1st
‘𝑧),
0R〉) |
81 | | ltresr 7761 |
. . . . . . . . . 10
⊢
(〈𝑎,
0R〉 <ℝ 〈(1st
‘𝑧),
0R〉 ↔ 𝑎 <R
(1st ‘𝑧)) |
82 | 80, 81 | sylib 121 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ 𝑎
<R (1st ‘𝑧)) |
83 | | breq2 3971 |
. . . . . . . . . 10
⊢ (𝑐 = (1st ‘𝑧) → (𝑎 <R 𝑐 ↔ 𝑎 <R
(1st ‘𝑧))) |
84 | 83 | rspcev 2816 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ 𝐵 ∧ 𝑎 <R
(1st ‘𝑧))
→ ∃𝑐 ∈
𝐵 𝑎 <R 𝑐) |
85 | 78, 82, 84 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ (𝑧 ∈ 𝐴 ∧ 〈𝑎, 0R〉
<ℝ 𝑧))
→ ∃𝑐 ∈
𝐵 𝑎 <R 𝑐) |
86 | 85 | rexlimdvaa 2575 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → (∃𝑧 ∈ 𝐴 〈𝑎, 0R〉
<ℝ 𝑧
→ ∃𝑐 ∈
𝐵 𝑎 <R 𝑐)) |
87 | | breq1 3970 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑐, 0R〉 →
(𝑧 <ℝ
〈𝑏,
0R〉 ↔ 〈𝑐, 0R〉
<ℝ 〈𝑏,
0R〉)) |
88 | | simplr 520 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
𝑏 ∈ R))
∧ 𝑎
<R 𝑏) ∧ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉) ∧ 𝑐 ∈ 𝐵) → ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉) |
89 | | simpr 109 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
𝑏 ∈ R))
∧ 𝑎
<R 𝑏) ∧ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵) |
90 | | opeq1 3743 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑐 → 〈𝑤, 0R〉 =
〈𝑐,
0R〉) |
91 | 90 | eleq1d 2226 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑐 → (〈𝑤, 0R〉 ∈
𝐴 ↔ 〈𝑐,
0R〉 ∈ 𝐴)) |
92 | 91, 11 | elrab2 2871 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ 𝐵 ↔ (𝑐 ∈ R ∧ 〈𝑐,
0R〉 ∈ 𝐴)) |
93 | 89, 92 | sylib 121 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
𝑏 ∈ R))
∧ 𝑎
<R 𝑏) ∧ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉) ∧ 𝑐 ∈ 𝐵) → (𝑐 ∈ R ∧ 〈𝑐,
0R〉 ∈ 𝐴)) |
94 | 93 | simprd 113 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
𝑏 ∈ R))
∧ 𝑎
<R 𝑏) ∧ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉) ∧ 𝑐 ∈ 𝐵) → 〈𝑐, 0R〉 ∈
𝐴) |
95 | 87, 88, 94 | rspcdva 2821 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
𝑏 ∈ R))
∧ 𝑎
<R 𝑏) ∧ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉) ∧ 𝑐 ∈ 𝐵) → 〈𝑐, 0R〉
<ℝ 〈𝑏,
0R〉) |
96 | | ltresr 7761 |
. . . . . . . . . 10
⊢
(〈𝑐,
0R〉 <ℝ 〈𝑏,
0R〉 ↔ 𝑐 <R 𝑏) |
97 | 95, 96 | sylib 121 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
𝑏 ∈ R))
∧ 𝑎
<R 𝑏) ∧ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉) ∧ 𝑐 ∈ 𝐵) → 𝑐 <R 𝑏) |
98 | 97 | ralrimiva 2530 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) ∧ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉) → ∀𝑐 ∈ 𝐵 𝑐 <R 𝑏) |
99 | 98 | ex 114 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → (∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉 → ∀𝑐 ∈ 𝐵 𝑐 <R 𝑏)) |
100 | 86, 99 | orim12d 776 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → ((∃𝑧 ∈ 𝐴 〈𝑎, 0R〉
<ℝ 𝑧
∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 〈𝑏,
0R〉) → (∃𝑐 ∈ 𝐵 𝑎 <R 𝑐 ∨ ∀𝑐 ∈ 𝐵 𝑐 <R 𝑏))) |
101 | 65, 100 | mpd 13 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) ∧
𝑎
<R 𝑏) → (∃𝑐 ∈ 𝐵 𝑎 <R 𝑐 ∨ ∀𝑐 ∈ 𝐵 𝑐 <R 𝑏)) |
102 | 101 | ex 114 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ R ∧ 𝑏 ∈ R)) →
(𝑎
<R 𝑏 → (∃𝑐 ∈ 𝐵 𝑎 <R 𝑐 ∨ ∀𝑐 ∈ 𝐵 𝑐 <R 𝑏))) |
103 | 102 | ralrimivva 2539 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ R ∀𝑏 ∈ R (𝑎 <R
𝑏 → (∃𝑐 ∈ 𝐵 𝑎 <R 𝑐 ∨ ∀𝑐 ∈ 𝐵 𝑐 <R 𝑏))) |
104 | 16, 40, 103 | suplocsr 7731 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ R (∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏 ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) |
105 | | simprl 521 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ R ∧ (∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏 ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐)))) → 𝑎 ∈ R) |
106 | 105, 58 | sylibr 133 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ R ∧ (∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏 ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐)))) → 〈𝑎,
0R〉 ∈ ℝ) |
107 | | breq2 3971 |
. . . . . . . 8
⊢ (𝑏 = (1st ‘𝑦) → (𝑎 <R 𝑏 ↔ 𝑎 <R
(1st ‘𝑦))) |
108 | 107 | notbid 657 |
. . . . . . 7
⊢ (𝑏 = (1st ‘𝑦) → (¬ 𝑎 <R
𝑏 ↔ ¬ 𝑎 <R
(1st ‘𝑦))) |
109 | | simplrr 526 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏)) ∧ 𝑦 ∈ 𝐴) → ∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏) |
110 | 1 | sselda 3128 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
111 | | elreal2 7752 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ ↔
((1st ‘𝑦)
∈ R ∧ 𝑦 = 〈(1st ‘𝑦),
0R〉)) |
112 | 110, 111 | sylib 121 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((1st ‘𝑦) ∈ R ∧
𝑦 = 〈(1st
‘𝑦),
0R〉)) |
113 | 112 | simpld 111 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (1st ‘𝑦) ∈
R) |
114 | 112 | simprd 113 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 = 〈(1st ‘𝑦),
0R〉) |
115 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
116 | 114, 115 | eqeltrrd 2235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 〈(1st ‘𝑦),
0R〉 ∈ 𝐴) |
117 | | opeq1 3743 |
. . . . . . . . . . 11
⊢ (𝑤 = (1st ‘𝑦) → 〈𝑤,
0R〉 = 〈(1st ‘𝑦),
0R〉) |
118 | 117 | eleq1d 2226 |
. . . . . . . . . 10
⊢ (𝑤 = (1st ‘𝑦) → (〈𝑤,
0R〉 ∈ 𝐴 ↔ 〈(1st ‘𝑦),
0R〉 ∈ 𝐴)) |
119 | 118, 11 | elrab2 2871 |
. . . . . . . . 9
⊢
((1st ‘𝑦) ∈ 𝐵 ↔ ((1st ‘𝑦) ∈ R ∧
〈(1st ‘𝑦), 0R〉 ∈
𝐴)) |
120 | 113, 116,
119 | sylanbrc 414 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (1st ‘𝑦) ∈ 𝐵) |
121 | 120 | adantlr 469 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏)) ∧ 𝑦 ∈ 𝐴) → (1st ‘𝑦) ∈ 𝐵) |
122 | 108, 109,
121 | rspcdva 2821 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏)) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑎 <R
(1st ‘𝑦)) |
123 | 114 | adantlr 469 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏)) ∧ 𝑦 ∈ 𝐴) → 𝑦 = 〈(1st ‘𝑦),
0R〉) |
124 | 123 | breq2d 3979 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏)) ∧ 𝑦 ∈ 𝐴) → (〈𝑎, 0R〉
<ℝ 𝑦
↔ 〈𝑎,
0R〉 <ℝ 〈(1st
‘𝑦),
0R〉)) |
125 | | ltresr 7761 |
. . . . . . 7
⊢
(〈𝑎,
0R〉 <ℝ 〈(1st
‘𝑦),
0R〉 ↔ 𝑎 <R
(1st ‘𝑦)) |
126 | 124, 125 | bitrdi 195 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏)) ∧ 𝑦 ∈ 𝐴) → (〈𝑎, 0R〉
<ℝ 𝑦
↔ 𝑎
<R (1st ‘𝑦))) |
127 | 122, 126 | mtbird 663 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏)) ∧ 𝑦 ∈ 𝐴) → ¬ 〈𝑎, 0R〉
<ℝ 𝑦) |
128 | 127 | ralrimiva 2530 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏)) → ∀𝑦 ∈ 𝐴 ¬ 〈𝑎, 0R〉
<ℝ 𝑦) |
129 | 128 | adantrrr 479 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ R ∧ (∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏 ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐)))) → ∀𝑦 ∈ 𝐴 ¬ 〈𝑎, 0R〉
<ℝ 𝑦) |
130 | | simplr 520 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → 𝑦 ∈ ℝ) |
131 | 130, 111 | sylib 121 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → ((1st ‘𝑦) ∈ R ∧
𝑦 = 〈(1st
‘𝑦),
0R〉)) |
132 | 131 | simprd 113 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → 𝑦 = 〈(1st ‘𝑦),
0R〉) |
133 | | simpr 109 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → 𝑦 <ℝ 〈𝑎,
0R〉) |
134 | 132, 133 | eqbrtrrd 3990 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → 〈(1st ‘𝑦),
0R〉 <ℝ 〈𝑎,
0R〉) |
135 | | ltresr 7761 |
. . . . . . . . 9
⊢
(〈(1st ‘𝑦), 0R〉
<ℝ 〈𝑎, 0R〉 ↔
(1st ‘𝑦)
<R 𝑎) |
136 | 134, 135 | sylib 121 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → (1st ‘𝑦) <R
𝑎) |
137 | | breq1 3970 |
. . . . . . . . . 10
⊢ (𝑏 = (1st ‘𝑦) → (𝑏 <R 𝑎 ↔ (1st
‘𝑦)
<R 𝑎)) |
138 | | breq1 3970 |
. . . . . . . . . . 11
⊢ (𝑏 = (1st ‘𝑦) → (𝑏 <R 𝑐 ↔ (1st
‘𝑦)
<R 𝑐)) |
139 | 138 | rexbidv 2458 |
. . . . . . . . . 10
⊢ (𝑏 = (1st ‘𝑦) → (∃𝑐 ∈ 𝐵 𝑏 <R 𝑐 ↔ ∃𝑐 ∈ 𝐵 (1st ‘𝑦) <R 𝑐)) |
140 | 137, 139 | imbi12d 233 |
. . . . . . . . 9
⊢ (𝑏 = (1st ‘𝑦) → ((𝑏 <R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐) ↔ ((1st
‘𝑦)
<R 𝑎 → ∃𝑐 ∈ 𝐵 (1st ‘𝑦) <R 𝑐))) |
141 | | simprr 522 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) → ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐)) |
142 | 141 | ad2antrr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → ∀𝑏 ∈ R (𝑏 <R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐)) |
143 | 131 | simpld 111 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → (1st ‘𝑦) ∈
R) |
144 | 140, 142,
143 | rspcdva 2821 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → ((1st ‘𝑦) <R
𝑎 → ∃𝑐 ∈ 𝐵 (1st ‘𝑦) <R 𝑐)) |
145 | 136, 144 | mpd 13 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → ∃𝑐 ∈ 𝐵 (1st ‘𝑦) <R 𝑐) |
146 | | nfv 1508 |
. . . . . . . . . . 11
⊢
Ⅎ𝑐𝜑 |
147 | | nfv 1508 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑐 𝑎 ∈
R |
148 | | nfcv 2299 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑐R |
149 | | nfv 1508 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑐 𝑏 <R
𝑎 |
150 | | nfre1 2500 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑐∃𝑐 ∈ 𝐵 𝑏 <R 𝑐 |
151 | 149, 150 | nfim 1552 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑐(𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐) |
152 | 148, 151 | nfralya 2497 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑐∀𝑏 ∈ R (𝑏 <R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐) |
153 | 147, 152 | nfan 1545 |
. . . . . . . . . . 11
⊢
Ⅎ𝑐(𝑎 ∈ R ∧
∀𝑏 ∈
R (𝑏
<R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐)) |
154 | 146, 153 | nfan 1545 |
. . . . . . . . . 10
⊢
Ⅎ𝑐(𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) |
155 | | nfv 1508 |
. . . . . . . . . 10
⊢
Ⅎ𝑐 𝑦 ∈ ℝ |
156 | 154, 155 | nfan 1545 |
. . . . . . . . 9
⊢
Ⅎ𝑐((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) |
157 | | nfv 1508 |
. . . . . . . . 9
⊢
Ⅎ𝑐 𝑦 <ℝ
〈𝑎,
0R〉 |
158 | 156, 157 | nfan 1545 |
. . . . . . . 8
⊢
Ⅎ𝑐(((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) |
159 | | nfv 1508 |
. . . . . . . 8
⊢
Ⅎ𝑐∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 |
160 | | simprl 521 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
∀𝑏 ∈
R (𝑏
<R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) ∧ (𝑐 ∈ 𝐵 ∧ (1st ‘𝑦) <R
𝑐)) → 𝑐 ∈ 𝐵) |
161 | 160, 92 | sylib 121 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
∀𝑏 ∈
R (𝑏
<R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) ∧ (𝑐 ∈ 𝐵 ∧ (1st ‘𝑦) <R
𝑐)) → (𝑐 ∈ R ∧
〈𝑐,
0R〉 ∈ 𝐴)) |
162 | 161 | simprd 113 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
∀𝑏 ∈
R (𝑏
<R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) ∧ (𝑐 ∈ 𝐵 ∧ (1st ‘𝑦) <R
𝑐)) → 〈𝑐,
0R〉 ∈ 𝐴) |
163 | 132 | adantr 274 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
∀𝑏 ∈
R (𝑏
<R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) ∧ (𝑐 ∈ 𝐵 ∧ (1st ‘𝑦) <R
𝑐)) → 𝑦 = 〈(1st
‘𝑦),
0R〉) |
164 | | simprr 522 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
∀𝑏 ∈
R (𝑏
<R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) ∧ (𝑐 ∈ 𝐵 ∧ (1st ‘𝑦) <R
𝑐)) → (1st
‘𝑦)
<R 𝑐) |
165 | | ltresr 7761 |
. . . . . . . . . . . 12
⊢
(〈(1st ‘𝑦), 0R〉
<ℝ 〈𝑐, 0R〉 ↔
(1st ‘𝑦)
<R 𝑐) |
166 | 164, 165 | sylibr 133 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
∀𝑏 ∈
R (𝑏
<R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) ∧ (𝑐 ∈ 𝐵 ∧ (1st ‘𝑦) <R
𝑐)) →
〈(1st ‘𝑦), 0R〉
<ℝ 〈𝑐,
0R〉) |
167 | 163, 166 | eqbrtrd 3988 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
∀𝑏 ∈
R (𝑏
<R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) ∧ (𝑐 ∈ 𝐵 ∧ (1st ‘𝑦) <R
𝑐)) → 𝑦 <ℝ
〈𝑐,
0R〉) |
168 | | breq2 3971 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑐, 0R〉 →
(𝑦 <ℝ
𝑧 ↔ 𝑦 <ℝ 〈𝑐,
0R〉)) |
169 | 168 | rspcev 2816 |
. . . . . . . . . 10
⊢
((〈𝑐,
0R〉 ∈ 𝐴 ∧ 𝑦 <ℝ 〈𝑐,
0R〉) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) |
170 | 162, 167,
169 | syl2anc 409 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑎 ∈ R ∧
∀𝑏 ∈
R (𝑏
<R 𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) ∧ (𝑐 ∈ 𝐵 ∧ (1st ‘𝑦) <R
𝑐)) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) |
171 | 170 | exp32 363 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → (𝑐 ∈ 𝐵 → ((1st ‘𝑦) <R
𝑐 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
172 | 158, 159,
171 | rexlimd 2571 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → (∃𝑐 ∈ 𝐵 (1st ‘𝑦) <R 𝑐 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
173 | 145, 172 | mpd 13 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 <ℝ 〈𝑎,
0R〉) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) |
174 | 173 | ex 114 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) ∧ 𝑦 ∈ ℝ) → (𝑦 <ℝ 〈𝑎,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
175 | 174 | ralrimiva 2530 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ R ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐))) → ∀𝑦 ∈ ℝ (𝑦 <ℝ
〈𝑎,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
176 | 175 | adantrrl 478 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ R ∧ (∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏 ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐)))) → ∀𝑦 ∈ ℝ (𝑦 <ℝ
〈𝑎,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
177 | 49 | notbid 657 |
. . . . . 6
⊢ (𝑥 = 〈𝑎, 0R〉 →
(¬ 𝑥
<ℝ 𝑦
↔ ¬ 〈𝑎,
0R〉 <ℝ 𝑦)) |
178 | 177 | ralbidv 2457 |
. . . . 5
⊢ (𝑥 = 〈𝑎, 0R〉 →
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 〈𝑎, 0R〉
<ℝ 𝑦)) |
179 | | breq2 3971 |
. . . . . . 7
⊢ (𝑥 = 〈𝑎, 0R〉 →
(𝑦 <ℝ
𝑥 ↔ 𝑦 <ℝ 〈𝑎,
0R〉)) |
180 | 179 | imbi1d 230 |
. . . . . 6
⊢ (𝑥 = 〈𝑎, 0R〉 →
((𝑦 <ℝ
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) ↔ (𝑦 <ℝ 〈𝑎,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
181 | 180 | ralbidv 2457 |
. . . . 5
⊢ (𝑥 = 〈𝑎, 0R〉 →
(∀𝑦 ∈ ℝ
(𝑦 <ℝ
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 <ℝ 〈𝑎,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
182 | 178, 181 | anbi12d 465 |
. . . 4
⊢ (𝑥 = 〈𝑎, 0R〉 →
((∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 〈𝑎, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑎, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
183 | 182 | rspcev 2816 |
. . 3
⊢
((〈𝑎,
0R〉 ∈ ℝ ∧ (∀𝑦 ∈ 𝐴 ¬ 〈𝑎, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑎, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
184 | 106, 129,
176, 183 | syl12anc 1218 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ R ∧ (∀𝑏 ∈ 𝐵 ¬ 𝑎 <R 𝑏 ∧ ∀𝑏 ∈ R (𝑏 <R
𝑎 → ∃𝑐 ∈ 𝐵 𝑏 <R 𝑐)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
185 | 104, 184 | rexlimddv 2579 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |