Step | Hyp | Ref
| Expression |
1 | | elreal2 10632 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↔
((1st ‘𝑥)
∈ R ∧ 𝑥 = 〈(1st ‘𝑥),
0R〉)) |
2 | 1 | simplbi 501 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
(1st ‘𝑥)
∈ R) |
3 | 2 | adantl 485 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) →
(1st ‘𝑥)
∈ R) |
4 | | fo1st 7734 |
. . . . . . . . . . . 12
⊢
1st :V–onto→V |
5 | | fof 6592 |
. . . . . . . . . . . 12
⊢
(1st :V–onto→V → 1st
:V⟶V) |
6 | | ffn 6504 |
. . . . . . . . . . . 12
⊢
(1st :V⟶V → 1st Fn V) |
7 | 4, 5, 6 | mp2b 10 |
. . . . . . . . . . 11
⊢
1st Fn V |
8 | | ssv 3901 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ V |
9 | | fvelimab 6741 |
. . . . . . . . . . 11
⊢
((1st Fn V ∧ 𝐴 ⊆ V) → (𝑤 ∈ (1st “ 𝐴) ↔ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤)) |
10 | 7, 8, 9 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (1st “
𝐴) ↔ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤) |
11 | | r19.29 3167 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝐴 𝑦 <ℝ 𝑥 ∧ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤) → ∃𝑦 ∈ 𝐴 (𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤)) |
12 | | ssel2 3872 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
13 | | ltresr2 10641 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 <ℝ 𝑥 ↔ (1st
‘𝑦)
<R (1st ‘𝑥))) |
14 | | breq1 5033 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑦) = 𝑤 → ((1st ‘𝑦) <R
(1st ‘𝑥)
↔ 𝑤
<R (1st ‘𝑥))) |
15 | 13, 14 | sylan9bb 513 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧
(1st ‘𝑦) =
𝑤) → (𝑦 <ℝ 𝑥 ↔ 𝑤 <R
(1st ‘𝑥))) |
16 | 15 | biimpd 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧
(1st ‘𝑦) =
𝑤) → (𝑦 <ℝ 𝑥 → 𝑤 <R
(1st ‘𝑥))) |
17 | 16 | exp31 423 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ → (𝑥 ∈ ℝ →
((1st ‘𝑦)
= 𝑤 → (𝑦 <ℝ 𝑥 → 𝑤 <R
(1st ‘𝑥))))) |
18 | 12, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ ℝ → ((1st
‘𝑦) = 𝑤 → (𝑦 <ℝ 𝑥 → 𝑤 <R
(1st ‘𝑥))))) |
19 | 18 | imp4b 425 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (((1st
‘𝑦) = 𝑤 ∧ 𝑦 <ℝ 𝑥) → 𝑤 <R
(1st ‘𝑥))) |
20 | 19 | ancomsd 469 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
21 | 20 | an32s 652 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → ((𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
22 | 21 | rexlimdva 3194 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∃𝑦 ∈ 𝐴 (𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
23 | 11, 22 | syl5 34 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
((∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
24 | 23 | expd 419 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → (∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤 → 𝑤 <R
(1st ‘𝑥)))) |
25 | 10, 24 | syl7bi 258 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → (𝑤 ∈ (1st “ 𝐴) → 𝑤 <R
(1st ‘𝑥)))) |
26 | 25 | impr 458 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → (𝑤 ∈ (1st “ 𝐴) → 𝑤 <R
(1st ‘𝑥))) |
27 | 26 | adantlr 715 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → (𝑤 ∈ (1st “ 𝐴) → 𝑤 <R
(1st ‘𝑥))) |
28 | 27 | ralrimiv 3095 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → ∀𝑤 ∈ (1st “ 𝐴)𝑤 <R
(1st ‘𝑥)) |
29 | 28 | expr 460 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∀𝑤 ∈ (1st “ 𝐴)𝑤 <R
(1st ‘𝑥))) |
30 | | brralrspcev 5090 |
. . . . 5
⊢
(((1st ‘𝑥) ∈ R ∧ ∀𝑤 ∈ (1st “
𝐴)𝑤 <R
(1st ‘𝑥))
→ ∃𝑣 ∈
R ∀𝑤
∈ (1st “ 𝐴)𝑤 <R 𝑣) |
31 | 3, 29, 30 | syl6an 684 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∃𝑣 ∈ R ∀𝑤 ∈ (1st “
𝐴)𝑤 <R 𝑣)) |
32 | 31 | rexlimdva 3194 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∃𝑣 ∈ R ∀𝑤 ∈ (1st “
𝐴)𝑤 <R 𝑣)) |
33 | | n0 4235 |
. . . . . 6
⊢ (𝐴 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐴) |
34 | | fnfvima 7006 |
. . . . . . . . 9
⊢
((1st Fn V ∧ 𝐴 ⊆ V ∧ 𝑦 ∈ 𝐴) → (1st ‘𝑦) ∈ (1st “
𝐴)) |
35 | 7, 8, 34 | mp3an12 1452 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (1st ‘𝑦) ∈ (1st “
𝐴)) |
36 | 35 | ne0d 4224 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → (1st “ 𝐴) ≠ ∅) |
37 | 36 | exlimiv 1937 |
. . . . . 6
⊢
(∃𝑦 𝑦 ∈ 𝐴 → (1st “ 𝐴) ≠ ∅) |
38 | 33, 37 | sylbi 220 |
. . . . 5
⊢ (𝐴 ≠ ∅ →
(1st “ 𝐴)
≠ ∅) |
39 | | supsr 10612 |
. . . . . 6
⊢
(((1st “ 𝐴) ≠ ∅ ∧ ∃𝑣 ∈ R
∀𝑤 ∈
(1st “ 𝐴)𝑤 <R 𝑣) → ∃𝑣 ∈ R
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢))) |
40 | 39 | ex 416 |
. . . . 5
⊢
((1st “ 𝐴) ≠ ∅ → (∃𝑣 ∈ R
∀𝑤 ∈
(1st “ 𝐴)𝑤 <R 𝑣 → ∃𝑣 ∈ R
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)))) |
41 | 38, 40 | syl 17 |
. . . 4
⊢ (𝐴 ≠ ∅ →
(∃𝑣 ∈
R ∀𝑤
∈ (1st “ 𝐴)𝑤 <R 𝑣 → ∃𝑣 ∈ R
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)))) |
42 | 41 | adantl 485 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑣 ∈
R ∀𝑤
∈ (1st “ 𝐴)𝑤 <R 𝑣 → ∃𝑣 ∈ R
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)))) |
43 | | breq2 5034 |
. . . . . . . . . . . 12
⊢ (𝑤 = (1st ‘𝑦) → (𝑣 <R 𝑤 ↔ 𝑣 <R
(1st ‘𝑦))) |
44 | 43 | notbid 321 |
. . . . . . . . . . 11
⊢ (𝑤 = (1st ‘𝑦) → (¬ 𝑣 <R
𝑤 ↔ ¬ 𝑣 <R
(1st ‘𝑦))) |
45 | 44 | rspccv 3523 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 → ((1st ‘𝑦) ∈ (1st “
𝐴) → ¬ 𝑣 <R
(1st ‘𝑦))) |
46 | 35, 45 | syl5com 31 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → (∀𝑤 ∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R
(1st ‘𝑦))) |
47 | 46 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (∀𝑤 ∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R
(1st ‘𝑦))) |
48 | | elreal2 10632 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ ↔
((1st ‘𝑦)
∈ R ∧ 𝑦 = 〈(1st ‘𝑦),
0R〉)) |
49 | 48 | simprbi 500 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → 𝑦 = 〈(1st
‘𝑦),
0R〉) |
50 | 49 | breq2d 5042 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ →
(〈𝑣,
0R〉 <ℝ 𝑦 ↔ 〈𝑣, 0R〉
<ℝ 〈(1st ‘𝑦),
0R〉)) |
51 | | ltresr 10640 |
. . . . . . . . . . 11
⊢
(〈𝑣,
0R〉 <ℝ 〈(1st
‘𝑦),
0R〉 ↔ 𝑣 <R
(1st ‘𝑦)) |
52 | 50, 51 | bitrdi 290 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ →
(〈𝑣,
0R〉 <ℝ 𝑦 ↔ 𝑣 <R
(1st ‘𝑦))) |
53 | 12, 52 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (〈𝑣, 0R〉
<ℝ 𝑦
↔ 𝑣
<R (1st ‘𝑦))) |
54 | 53 | notbid 321 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (¬ 〈𝑣, 0R〉
<ℝ 𝑦
↔ ¬ 𝑣
<R (1st ‘𝑦))) |
55 | 47, 54 | sylibrd 262 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (∀𝑤 ∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 → ¬ 〈𝑣,
0R〉 <ℝ 𝑦)) |
56 | 55 | ralrimdva 3101 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 → ∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦)) |
57 | 56 | ad2antrr 726 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 → ∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦)) |
58 | 49 | breq1d 5040 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → (𝑦 <ℝ
〈𝑣,
0R〉 ↔ 〈(1st ‘𝑦),
0R〉 <ℝ 〈𝑣,
0R〉)) |
59 | | ltresr 10640 |
. . . . . . . . . . . . . 14
⊢
(〈(1st ‘𝑦), 0R〉
<ℝ 〈𝑣, 0R〉 ↔
(1st ‘𝑦)
<R 𝑣) |
60 | 58, 59 | bitrdi 290 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → (𝑦 <ℝ
〈𝑣,
0R〉 ↔ (1st ‘𝑦) <R
𝑣)) |
61 | 48 | simplbi 501 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ →
(1st ‘𝑦)
∈ R) |
62 | | breq1 5033 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (1st ‘𝑦) → (𝑤 <R 𝑣 ↔ (1st
‘𝑦)
<R 𝑣)) |
63 | | breq1 5033 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (1st ‘𝑦) → (𝑤 <R 𝑢 ↔ (1st
‘𝑦)
<R 𝑢)) |
64 | 63 | rexbidv 3207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (1st ‘𝑦) → (∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢 ↔ ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢)) |
65 | 62, 64 | imbi12d 348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (1st ‘𝑦) → ((𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) ↔ ((1st
‘𝑦)
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)(1st ‘𝑦) <R
𝑢))) |
66 | 65 | rspccv 3523 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → ((1st
‘𝑦) ∈
R → ((1st ‘𝑦) <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢))) |
67 | 61, 66 | syl5 34 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → ((1st
‘𝑦)
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)(1st ‘𝑦) <R
𝑢))) |
68 | 67 | com3l 89 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ →
((1st ‘𝑦)
<R 𝑣 → (∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢))) |
69 | 60, 68 | sylbid 243 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → (𝑦 <ℝ
〈𝑣,
0R〉 → (∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢))) |
70 | 69 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑦 <ℝ
〈𝑣,
0R〉 → (∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢))) |
71 | | fvelimab 6741 |
. . . . . . . . . . . . . . . 16
⊢
((1st Fn V ∧ 𝐴 ⊆ V) → (𝑢 ∈ (1st “ 𝐴) ↔ ∃𝑧 ∈ 𝐴 (1st ‘𝑧) = 𝑢)) |
72 | 7, 8, 71 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (1st “
𝐴) ↔ ∃𝑧 ∈ 𝐴 (1st ‘𝑧) = 𝑢) |
73 | | ssel2 3872 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
74 | | ltresr2 10641 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 <ℝ 𝑧 ↔ (1st
‘𝑦)
<R (1st ‘𝑧))) |
75 | 73, 74 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 <ℝ 𝑧 ↔ (1st ‘𝑦) <R
(1st ‘𝑧))) |
76 | | breq2 5034 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑧) = 𝑢 → ((1st ‘𝑦) <R
(1st ‘𝑧)
↔ (1st ‘𝑦) <R 𝑢)) |
77 | 75, 76 | sylan9bb 513 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴)) ∧ (1st ‘𝑧) = 𝑢) → (𝑦 <ℝ 𝑧 ↔ (1st ‘𝑦) <R
𝑢)) |
78 | 77 | exbiri 811 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴)) → ((1st ‘𝑧) = 𝑢 → ((1st ‘𝑦) <R
𝑢 → 𝑦 <ℝ 𝑧))) |
79 | 78 | expr 460 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧 ∈ 𝐴 → ((1st ‘𝑧) = 𝑢 → ((1st ‘𝑦) <R
𝑢 → 𝑦 <ℝ 𝑧)))) |
80 | 79 | com4r 94 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑦) <R 𝑢 → ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧 ∈ 𝐴 → ((1st ‘𝑧) = 𝑢 → 𝑦 <ℝ 𝑧)))) |
81 | 80 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑧 ∈ 𝐴 → ((1st ‘𝑧) = 𝑢 → 𝑦 <ℝ 𝑧))) |
82 | 81 | reximdvai 3182 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (∃𝑧 ∈ 𝐴 (1st ‘𝑧) = 𝑢 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
83 | 72, 82 | syl5bi 245 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑢 ∈ (1st “
𝐴) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
84 | 83 | expcom 417 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) →
((1st ‘𝑦)
<R 𝑢 → (𝑢 ∈ (1st “ 𝐴) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
85 | 84 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑢 ∈ (1st “
𝐴) → ((1st
‘𝑦)
<R 𝑢 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
86 | 85 | rexlimdv 3193 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) →
(∃𝑢 ∈
(1st “ 𝐴)(1st ‘𝑦) <R 𝑢 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
87 | 70, 86 | syl6d 75 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑦 <ℝ
〈𝑣,
0R〉 → (∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
88 | 87 | com23 86 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
89 | 88 | ex 416 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → (𝐴 ⊆ ℝ →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
90 | 89 | com3l 89 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
91 | 90 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
92 | 91 | ralrimdv 3100 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → ∀𝑦 ∈ ℝ (𝑦 <ℝ
〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
93 | | opelreal 10630 |
. . . . . . . 8
⊢
(〈𝑣,
0R〉 ∈ ℝ ↔ 𝑣 ∈ R) |
94 | 93 | biimpri 231 |
. . . . . . 7
⊢ (𝑣 ∈ R →
〈𝑣,
0R〉 ∈ ℝ) |
95 | 94 | adantl 485 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
〈𝑣,
0R〉 ∈ ℝ) |
96 | | breq1 5033 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑣, 0R〉 →
(𝑥 <ℝ
𝑦 ↔ 〈𝑣,
0R〉 <ℝ 𝑦)) |
97 | 96 | notbid 321 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑣, 0R〉 →
(¬ 𝑥
<ℝ 𝑦
↔ ¬ 〈𝑣,
0R〉 <ℝ 𝑦)) |
98 | 97 | ralbidv 3109 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑣, 0R〉 →
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦)) |
99 | | breq2 5034 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑣, 0R〉 →
(𝑦 <ℝ
𝑥 ↔ 𝑦 <ℝ 〈𝑣,
0R〉)) |
100 | 99 | imbi1d 345 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑣, 0R〉 →
((𝑦 <ℝ
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) ↔ (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
101 | 100 | ralbidv 3109 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑣, 0R〉 →
(∀𝑦 ∈ ℝ
(𝑦 <ℝ
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
102 | 98, 101 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑣, 0R〉 →
((∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
103 | 102 | rspcev 3526 |
. . . . . . 7
⊢
((〈𝑣,
0R〉 ∈ ℝ ∧ (∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
104 | 103 | ex 416 |
. . . . . 6
⊢
(〈𝑣,
0R〉 ∈ ℝ → ((∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
105 | 95, 104 | syl 17 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
((∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
106 | 57, 92, 105 | syl2and 611 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
((∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
107 | 106 | rexlimdva 3194 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑣 ∈
R (∀𝑤
∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R
𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
108 | 32, 42, 107 | 3syld 60 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
109 | 108 | 3impia 1118 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |