Step | Hyp | Ref
| Expression |
1 | | elreal2 9832 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↔
((1st ‘𝑥)
∈ R ∧ 𝑥 = 〈(1st ‘𝑥),
0R〉)) |
2 | 1 | simplbi 475 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
(1st ‘𝑥)
∈ R) |
3 | 2 | adantl 481 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) →
(1st ‘𝑥)
∈ R) |
4 | | fo1st 7079 |
. . . . . . . . . . . 12
⊢
1st :V–onto→V |
5 | | fof 6028 |
. . . . . . . . . . . 12
⊢
(1st :V–onto→V → 1st
:V⟶V) |
6 | | ffn 5958 |
. . . . . . . . . . . 12
⊢
(1st :V⟶V → 1st Fn V) |
7 | 4, 5, 6 | mp2b 10 |
. . . . . . . . . . 11
⊢
1st Fn V |
8 | | ssv 3588 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ V |
9 | | fvelimab 6163 |
. . . . . . . . . . 11
⊢
((1st Fn V ∧ 𝐴 ⊆ V) → (𝑤 ∈ (1st “ 𝐴) ↔ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤)) |
10 | 7, 8, 9 | mp2an 704 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (1st “
𝐴) ↔ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤) |
11 | | r19.29 3054 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝐴 𝑦 <ℝ 𝑥 ∧ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤) → ∃𝑦 ∈ 𝐴 (𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤)) |
12 | | ssel2 3563 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
13 | | ltresr2 9841 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 <ℝ 𝑥 ↔ (1st
‘𝑦)
<R (1st ‘𝑥))) |
14 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑦) = 𝑤 → ((1st ‘𝑦) <R
(1st ‘𝑥)
↔ 𝑤
<R (1st ‘𝑥))) |
15 | 13, 14 | sylan9bb 732 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧
(1st ‘𝑦) =
𝑤) → (𝑦 <ℝ 𝑥 ↔ 𝑤 <R
(1st ‘𝑥))) |
16 | 15 | biimpd 218 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧
(1st ‘𝑦) =
𝑤) → (𝑦 <ℝ 𝑥 → 𝑤 <R
(1st ‘𝑥))) |
17 | 16 | exp31 628 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ → (𝑥 ∈ ℝ →
((1st ‘𝑦)
= 𝑤 → (𝑦 <ℝ 𝑥 → 𝑤 <R
(1st ‘𝑥))))) |
18 | 12, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ ℝ → ((1st
‘𝑦) = 𝑤 → (𝑦 <ℝ 𝑥 → 𝑤 <R
(1st ‘𝑥))))) |
19 | 18 | imp4b 611 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (((1st
‘𝑦) = 𝑤 ∧ 𝑦 <ℝ 𝑥) → 𝑤 <R
(1st ‘𝑥))) |
20 | 19 | ancomsd 469 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
21 | 20 | an32s 842 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → ((𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
22 | 21 | rexlimdva 3013 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∃𝑦 ∈ 𝐴 (𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
23 | 11, 22 | syl5 33 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
((∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
24 | 23 | expd 451 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → (∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤 → 𝑤 <R
(1st ‘𝑥)))) |
25 | 10, 24 | syl7bi 244 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → (𝑤 ∈ (1st “ 𝐴) → 𝑤 <R
(1st ‘𝑥)))) |
26 | 25 | impr 647 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → (𝑤 ∈ (1st “ 𝐴) → 𝑤 <R
(1st ‘𝑥))) |
27 | 26 | adantlr 747 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → (𝑤 ∈ (1st “ 𝐴) → 𝑤 <R
(1st ‘𝑥))) |
28 | 27 | ralrimiv 2948 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → ∀𝑤 ∈ (1st “ 𝐴)𝑤 <R
(1st ‘𝑥)) |
29 | 28 | expr 641 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∀𝑤 ∈ (1st “ 𝐴)𝑤 <R
(1st ‘𝑥))) |
30 | | breq2 4587 |
. . . . . . 7
⊢ (𝑣 = (1st ‘𝑥) → (𝑤 <R 𝑣 ↔ 𝑤 <R
(1st ‘𝑥))) |
31 | 30 | ralbidv 2969 |
. . . . . 6
⊢ (𝑣 = (1st ‘𝑥) → (∀𝑤 ∈ (1st “
𝐴)𝑤 <R 𝑣 ↔ ∀𝑤 ∈ (1st “
𝐴)𝑤 <R
(1st ‘𝑥))) |
32 | 31 | rspcev 3282 |
. . . . 5
⊢
(((1st ‘𝑥) ∈ R ∧ ∀𝑤 ∈ (1st “
𝐴)𝑤 <R
(1st ‘𝑥))
→ ∃𝑣 ∈
R ∀𝑤
∈ (1st “ 𝐴)𝑤 <R 𝑣) |
33 | 3, 29, 32 | syl6an 566 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∃𝑣 ∈ R ∀𝑤 ∈ (1st “
𝐴)𝑤 <R 𝑣)) |
34 | 33 | rexlimdva 3013 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∃𝑣 ∈ R ∀𝑤 ∈ (1st “
𝐴)𝑤 <R 𝑣)) |
35 | | n0 3890 |
. . . . . 6
⊢ (𝐴 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐴) |
36 | | fnfvima 6400 |
. . . . . . . . 9
⊢
((1st Fn V ∧ 𝐴 ⊆ V ∧ 𝑦 ∈ 𝐴) → (1st ‘𝑦) ∈ (1st “
𝐴)) |
37 | 7, 8, 36 | mp3an12 1406 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (1st ‘𝑦) ∈ (1st “
𝐴)) |
38 | | ne0i 3880 |
. . . . . . . 8
⊢
((1st ‘𝑦) ∈ (1st “ 𝐴) → (1st “
𝐴) ≠
∅) |
39 | 37, 38 | syl 17 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → (1st “ 𝐴) ≠ ∅) |
40 | 39 | exlimiv 1845 |
. . . . . 6
⊢
(∃𝑦 𝑦 ∈ 𝐴 → (1st “ 𝐴) ≠ ∅) |
41 | 35, 40 | sylbi 206 |
. . . . 5
⊢ (𝐴 ≠ ∅ →
(1st “ 𝐴)
≠ ∅) |
42 | | supsr 9812 |
. . . . . 6
⊢
(((1st “ 𝐴) ≠ ∅ ∧ ∃𝑣 ∈ R
∀𝑤 ∈
(1st “ 𝐴)𝑤 <R 𝑣) → ∃𝑣 ∈ R
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢))) |
43 | 42 | ex 449 |
. . . . 5
⊢
((1st “ 𝐴) ≠ ∅ → (∃𝑣 ∈ R
∀𝑤 ∈
(1st “ 𝐴)𝑤 <R 𝑣 → ∃𝑣 ∈ R
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)))) |
44 | 41, 43 | syl 17 |
. . . 4
⊢ (𝐴 ≠ ∅ →
(∃𝑣 ∈
R ∀𝑤
∈ (1st “ 𝐴)𝑤 <R 𝑣 → ∃𝑣 ∈ R
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)))) |
45 | 44 | adantl 481 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑣 ∈
R ∀𝑤
∈ (1st “ 𝐴)𝑤 <R 𝑣 → ∃𝑣 ∈ R
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)))) |
46 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑤 = (1st ‘𝑦) → (𝑣 <R 𝑤 ↔ 𝑣 <R
(1st ‘𝑦))) |
47 | 46 | notbid 307 |
. . . . . . . . . . 11
⊢ (𝑤 = (1st ‘𝑦) → (¬ 𝑣 <R
𝑤 ↔ ¬ 𝑣 <R
(1st ‘𝑦))) |
48 | 47 | rspccv 3279 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 → ((1st ‘𝑦) ∈ (1st “
𝐴) → ¬ 𝑣 <R
(1st ‘𝑦))) |
49 | 37, 48 | syl5com 31 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → (∀𝑤 ∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R
(1st ‘𝑦))) |
50 | 49 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (∀𝑤 ∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R
(1st ‘𝑦))) |
51 | | elreal2 9832 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ ↔
((1st ‘𝑦)
∈ R ∧ 𝑦 = 〈(1st ‘𝑦),
0R〉)) |
52 | 51 | simprbi 479 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → 𝑦 = 〈(1st
‘𝑦),
0R〉) |
53 | 52 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ →
(〈𝑣,
0R〉 <ℝ 𝑦 ↔ 〈𝑣, 0R〉
<ℝ 〈(1st ‘𝑦),
0R〉)) |
54 | | ltresr 9840 |
. . . . . . . . . . 11
⊢
(〈𝑣,
0R〉 <ℝ 〈(1st
‘𝑦),
0R〉 ↔ 𝑣 <R
(1st ‘𝑦)) |
55 | 53, 54 | syl6bb 275 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ →
(〈𝑣,
0R〉 <ℝ 𝑦 ↔ 𝑣 <R
(1st ‘𝑦))) |
56 | 12, 55 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (〈𝑣, 0R〉
<ℝ 𝑦
↔ 𝑣
<R (1st ‘𝑦))) |
57 | 56 | notbid 307 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (¬ 〈𝑣, 0R〉
<ℝ 𝑦
↔ ¬ 𝑣
<R (1st ‘𝑦))) |
58 | 50, 57 | sylibrd 248 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (∀𝑤 ∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 → ¬ 〈𝑣,
0R〉 <ℝ 𝑦)) |
59 | 58 | ralrimdva 2952 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 → ∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦)) |
60 | 59 | ad2antrr 758 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 → ∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦)) |
61 | 52 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → (𝑦 <ℝ
〈𝑣,
0R〉 ↔ 〈(1st ‘𝑦),
0R〉 <ℝ 〈𝑣,
0R〉)) |
62 | | ltresr 9840 |
. . . . . . . . . . . . . 14
⊢
(〈(1st ‘𝑦), 0R〉
<ℝ 〈𝑣, 0R〉 ↔
(1st ‘𝑦)
<R 𝑣) |
63 | 61, 62 | syl6bb 275 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → (𝑦 <ℝ
〈𝑣,
0R〉 ↔ (1st ‘𝑦) <R
𝑣)) |
64 | 51 | simplbi 475 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ →
(1st ‘𝑦)
∈ R) |
65 | | breq1 4586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (1st ‘𝑦) → (𝑤 <R 𝑣 ↔ (1st
‘𝑦)
<R 𝑣)) |
66 | | breq1 4586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (1st ‘𝑦) → (𝑤 <R 𝑢 ↔ (1st
‘𝑦)
<R 𝑢)) |
67 | 66 | rexbidv 3034 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (1st ‘𝑦) → (∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢 ↔ ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢)) |
68 | 65, 67 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (1st ‘𝑦) → ((𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) ↔ ((1st
‘𝑦)
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)(1st ‘𝑦) <R
𝑢))) |
69 | 68 | rspccv 3279 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → ((1st
‘𝑦) ∈
R → ((1st ‘𝑦) <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢))) |
70 | 64, 69 | syl5 33 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → ((1st
‘𝑦)
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)(1st ‘𝑦) <R
𝑢))) |
71 | 70 | com3l 87 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ →
((1st ‘𝑦)
<R 𝑣 → (∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢))) |
72 | 63, 71 | sylbid 229 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → (𝑦 <ℝ
〈𝑣,
0R〉 → (∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢))) |
73 | 72 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑦 <ℝ
〈𝑣,
0R〉 → (∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢))) |
74 | | fvelimab 6163 |
. . . . . . . . . . . . . . . 16
⊢
((1st Fn V ∧ 𝐴 ⊆ V) → (𝑢 ∈ (1st “ 𝐴) ↔ ∃𝑧 ∈ 𝐴 (1st ‘𝑧) = 𝑢)) |
75 | 7, 8, 74 | mp2an 704 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (1st “
𝐴) ↔ ∃𝑧 ∈ 𝐴 (1st ‘𝑧) = 𝑢) |
76 | | ssel2 3563 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
77 | | ltresr2 9841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 <ℝ 𝑧 ↔ (1st
‘𝑦)
<R (1st ‘𝑧))) |
78 | 76, 77 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 <ℝ 𝑧 ↔ (1st ‘𝑦) <R
(1st ‘𝑧))) |
79 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑧) = 𝑢 → ((1st ‘𝑦) <R
(1st ‘𝑧)
↔ (1st ‘𝑦) <R 𝑢)) |
80 | 78, 79 | sylan9bb 732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴)) ∧ (1st ‘𝑧) = 𝑢) → (𝑦 <ℝ 𝑧 ↔ (1st ‘𝑦) <R
𝑢)) |
81 | 80 | exbiri 650 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴)) → ((1st ‘𝑧) = 𝑢 → ((1st ‘𝑦) <R
𝑢 → 𝑦 <ℝ 𝑧))) |
82 | 81 | expr 641 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧 ∈ 𝐴 → ((1st ‘𝑧) = 𝑢 → ((1st ‘𝑦) <R
𝑢 → 𝑦 <ℝ 𝑧)))) |
83 | 82 | com4r 92 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑦) <R 𝑢 → ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧 ∈ 𝐴 → ((1st ‘𝑧) = 𝑢 → 𝑦 <ℝ 𝑧)))) |
84 | 83 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑧 ∈ 𝐴 → ((1st ‘𝑧) = 𝑢 → 𝑦 <ℝ 𝑧))) |
85 | 84 | reximdvai 2998 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (∃𝑧 ∈ 𝐴 (1st ‘𝑧) = 𝑢 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
86 | 75, 85 | syl5bi 231 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑢 ∈ (1st “
𝐴) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
87 | 86 | expcom 450 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) →
((1st ‘𝑦)
<R 𝑢 → (𝑢 ∈ (1st “ 𝐴) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
88 | 87 | com23 84 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑢 ∈ (1st “
𝐴) → ((1st
‘𝑦)
<R 𝑢 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
89 | 88 | rexlimdv 3012 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) →
(∃𝑢 ∈
(1st “ 𝐴)(1st ‘𝑦) <R 𝑢 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
90 | 73, 89 | syl6d 73 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑦 <ℝ
〈𝑣,
0R〉 → (∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
91 | 90 | com23 84 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
92 | 91 | ex 449 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → (𝐴 ⊆ ℝ →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
93 | 92 | com3l 87 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
94 | 93 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → (𝑦 ∈ ℝ → (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
95 | 94 | ralrimdv 2951 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → ∀𝑦 ∈ ℝ (𝑦 <ℝ
〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
96 | | opelreal 9830 |
. . . . . . . 8
⊢
(〈𝑣,
0R〉 ∈ ℝ ↔ 𝑣 ∈ R) |
97 | 96 | biimpri 217 |
. . . . . . 7
⊢ (𝑣 ∈ R →
〈𝑣,
0R〉 ∈ ℝ) |
98 | 97 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
〈𝑣,
0R〉 ∈ ℝ) |
99 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑣, 0R〉 →
(𝑥 <ℝ
𝑦 ↔ 〈𝑣,
0R〉 <ℝ 𝑦)) |
100 | 99 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑣, 0R〉 →
(¬ 𝑥
<ℝ 𝑦
↔ ¬ 〈𝑣,
0R〉 <ℝ 𝑦)) |
101 | 100 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑣, 0R〉 →
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦)) |
102 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑣, 0R〉 →
(𝑦 <ℝ
𝑥 ↔ 𝑦 <ℝ 〈𝑣,
0R〉)) |
103 | 102 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑣, 0R〉 →
((𝑦 <ℝ
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) ↔ (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
104 | 103 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑣, 0R〉 →
(∀𝑦 ∈ ℝ
(𝑦 <ℝ
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
105 | 101, 104 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑣, 0R〉 →
((∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
106 | 105 | rspcev 3282 |
. . . . . . 7
⊢
((〈𝑣,
0R〉 ∈ ℝ ∧ (∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
107 | 106 | ex 449 |
. . . . . 6
⊢
(〈𝑣,
0R〉 ∈ ℝ → ((∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
108 | 98, 107 | syl 17 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
((∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
109 | 60, 95, 108 | syl2and 499 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
((∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
110 | 109 | rexlimdva 3013 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑣 ∈
R (∀𝑤
∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R
𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
111 | 34, 45, 110 | 3syld 58 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
112 | 111 | 3impia 1253 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |