| Step | Hyp | Ref
| Expression |
| 1 | | elreal2 11172 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↔
((1st ‘𝑥)
∈ R ∧ 𝑥 = 〈(1st ‘𝑥),
0R〉)) |
| 2 | 1 | simplbi 497 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
(1st ‘𝑥)
∈ R) |
| 3 | 2 | adantl 481 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) →
(1st ‘𝑥)
∈ R) |
| 4 | | fo1st 8034 |
. . . . . . . . . . . 12
⊢
1st :V–onto→V |
| 5 | | fof 6820 |
. . . . . . . . . . . 12
⊢
(1st :V–onto→V → 1st
:V⟶V) |
| 6 | | ffn 6736 |
. . . . . . . . . . . 12
⊢
(1st :V⟶V → 1st Fn V) |
| 7 | 4, 5, 6 | mp2b 10 |
. . . . . . . . . . 11
⊢
1st Fn V |
| 8 | | ssv 4008 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ V |
| 9 | | fvelimab 6981 |
. . . . . . . . . . 11
⊢
((1st Fn V ∧ 𝐴 ⊆ V) → (𝑤 ∈ (1st “ 𝐴) ↔ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤)) |
| 10 | 7, 8, 9 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (1st “
𝐴) ↔ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤) |
| 11 | | r19.29 3114 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝐴 𝑦 <ℝ 𝑥 ∧ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤) → ∃𝑦 ∈ 𝐴 (𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤)) |
| 12 | | ssel2 3978 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
| 13 | | ltresr2 11181 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 <ℝ 𝑥 ↔ (1st
‘𝑦)
<R (1st ‘𝑥))) |
| 14 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑦) = 𝑤 → ((1st ‘𝑦) <R
(1st ‘𝑥)
↔ 𝑤
<R (1st ‘𝑥))) |
| 15 | 13, 14 | sylan9bb 509 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧
(1st ‘𝑦) =
𝑤) → (𝑦 <ℝ 𝑥 ↔ 𝑤 <R
(1st ‘𝑥))) |
| 16 | 15 | biimpd 229 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) ∧
(1st ‘𝑦) =
𝑤) → (𝑦 <ℝ 𝑥 → 𝑤 <R
(1st ‘𝑥))) |
| 17 | 16 | exp31 419 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ → (𝑥 ∈ ℝ →
((1st ‘𝑦)
= 𝑤 → (𝑦 <ℝ 𝑥 → 𝑤 <R
(1st ‘𝑥))))) |
| 18 | 12, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ ℝ → ((1st
‘𝑦) = 𝑤 → (𝑦 <ℝ 𝑥 → 𝑤 <R
(1st ‘𝑥))))) |
| 19 | 18 | imp4b 421 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → (((1st
‘𝑦) = 𝑤 ∧ 𝑦 <ℝ 𝑥) → 𝑤 <R
(1st ‘𝑥))) |
| 20 | 19 | ancomsd 465 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ ℝ) → ((𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
| 21 | 20 | an32s 652 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → ((𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
| 22 | 21 | rexlimdva 3155 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∃𝑦 ∈ 𝐴 (𝑦 <ℝ 𝑥 ∧ (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
| 23 | 11, 22 | syl5 34 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
((∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤) → 𝑤 <R
(1st ‘𝑥))) |
| 24 | 23 | expd 415 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → (∃𝑦 ∈ 𝐴 (1st ‘𝑦) = 𝑤 → 𝑤 <R
(1st ‘𝑥)))) |
| 25 | 10, 24 | syl7bi 255 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → (𝑤 ∈ (1st “ 𝐴) → 𝑤 <R
(1st ‘𝑥)))) |
| 26 | 25 | impr 454 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → (𝑤 ∈ (1st “ 𝐴) → 𝑤 <R
(1st ‘𝑥))) |
| 27 | 26 | adantlr 715 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → (𝑤 ∈ (1st “ 𝐴) → 𝑤 <R
(1st ‘𝑥))) |
| 28 | 27 | ralrimiv 3145 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ ℝ ∧
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)) → ∀𝑤 ∈ (1st “ 𝐴)𝑤 <R
(1st ‘𝑥)) |
| 29 | 28 | expr 456 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∀𝑤 ∈ (1st “ 𝐴)𝑤 <R
(1st ‘𝑥))) |
| 30 | | brralrspcev 5203 |
. . . . 5
⊢
(((1st ‘𝑥) ∈ R ∧ ∀𝑤 ∈ (1st “
𝐴)𝑤 <R
(1st ‘𝑥))
→ ∃𝑣 ∈
R ∀𝑤
∈ (1st “ 𝐴)𝑤 <R 𝑣) |
| 31 | 3, 29, 30 | syl6an 684 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∃𝑣 ∈ R ∀𝑤 ∈ (1st “
𝐴)𝑤 <R 𝑣)) |
| 32 | 31 | rexlimdva 3155 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∃𝑣 ∈ R ∀𝑤 ∈ (1st “
𝐴)𝑤 <R 𝑣)) |
| 33 | | n0 4353 |
. . . . . 6
⊢ (𝐴 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐴) |
| 34 | | fnfvima 7253 |
. . . . . . . . 9
⊢
((1st Fn V ∧ 𝐴 ⊆ V ∧ 𝑦 ∈ 𝐴) → (1st ‘𝑦) ∈ (1st “
𝐴)) |
| 35 | 7, 8, 34 | mp3an12 1453 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (1st ‘𝑦) ∈ (1st “
𝐴)) |
| 36 | 35 | ne0d 4342 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → (1st “ 𝐴) ≠ ∅) |
| 37 | 36 | exlimiv 1930 |
. . . . . 6
⊢
(∃𝑦 𝑦 ∈ 𝐴 → (1st “ 𝐴) ≠ ∅) |
| 38 | 33, 37 | sylbi 217 |
. . . . 5
⊢ (𝐴 ≠ ∅ →
(1st “ 𝐴)
≠ ∅) |
| 39 | | supsr 11152 |
. . . . . 6
⊢
(((1st “ 𝐴) ≠ ∅ ∧ ∃𝑣 ∈ R
∀𝑤 ∈
(1st “ 𝐴)𝑤 <R 𝑣) → ∃𝑣 ∈ R
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢))) |
| 40 | 39 | ex 412 |
. . . . 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 481 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑣 ∈
R ∀𝑤
∈ (1st “ 𝐴)𝑤 <R 𝑣 → ∃𝑣 ∈ R
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)))) |
| 43 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑤 = (1st ‘𝑦) → (𝑣 <R 𝑤 ↔ 𝑣 <R
(1st ‘𝑦))) |
| 44 | 43 | notbid 318 |
. . . . . . . . . . 11
⊢ (𝑤 = (1st ‘𝑦) → (¬ 𝑣 <R
𝑤 ↔ ¬ 𝑣 <R
(1st ‘𝑦))) |
| 45 | 44 | rspccv 3619 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 → ((1st ‘𝑦) ∈ (1st “
𝐴) → ¬ 𝑣 <R
(1st ‘𝑦))) |
| 46 | 35, 45 | syl5com 31 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → (∀𝑤 ∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R
(1st ‘𝑦))) |
| 47 | 46 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (∀𝑤 ∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R
(1st ‘𝑦))) |
| 48 | | elreal2 11172 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ ↔
((1st ‘𝑦)
∈ R ∧ 𝑦 = 〈(1st ‘𝑦),
0R〉)) |
| 49 | 48 | simprbi 496 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → 𝑦 = 〈(1st
‘𝑦),
0R〉) |
| 50 | 49 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ →
(〈𝑣,
0R〉 <ℝ 𝑦 ↔ 〈𝑣, 0R〉
<ℝ 〈(1st ‘𝑦),
0R〉)) |
| 51 | | ltresr 11180 |
. . . . . . . . . . 11
⊢
(〈𝑣,
0R〉 <ℝ 〈(1st
‘𝑦),
0R〉 ↔ 𝑣 <R
(1st ‘𝑦)) |
| 52 | 50, 51 | bitrdi 287 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ →
(〈𝑣,
0R〉 <ℝ 𝑦 ↔ 𝑣 <R
(1st ‘𝑦))) |
| 53 | 12, 52 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (〈𝑣, 0R〉
<ℝ 𝑦
↔ 𝑣
<R (1st ‘𝑦))) |
| 54 | 53 | notbid 318 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (¬ 〈𝑣, 0R〉
<ℝ 𝑦
↔ ¬ 𝑣
<R (1st ‘𝑦))) |
| 55 | 47, 54 | sylibrd 259 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴) → (∀𝑤 ∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 → ¬ 〈𝑣,
0R〉 <ℝ 𝑦)) |
| 56 | 55 | ralrimdva 3154 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ →
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 → ∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦)) |
| 57 | 56 | ad2antrr 726 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
(∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 → ∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦)) |
| 58 | 49 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → (𝑦 <ℝ
〈𝑣,
0R〉 ↔ 〈(1st ‘𝑦),
0R〉 <ℝ 〈𝑣,
0R〉)) |
| 59 | | ltresr 11180 |
. . . . . . . . . . . . . 14
⊢
(〈(1st ‘𝑦), 0R〉
<ℝ 〈𝑣, 0R〉 ↔
(1st ‘𝑦)
<R 𝑣) |
| 60 | 58, 59 | bitrdi 287 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → (𝑦 <ℝ
〈𝑣,
0R〉 ↔ (1st ‘𝑦) <R
𝑣)) |
| 61 | 48 | simplbi 497 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ →
(1st ‘𝑦)
∈ R) |
| 62 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (1st ‘𝑦) → (𝑤 <R 𝑣 ↔ (1st
‘𝑦)
<R 𝑣)) |
| 63 | | breq1 5146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (1st ‘𝑦) → (𝑤 <R 𝑢 ↔ (1st
‘𝑦)
<R 𝑢)) |
| 64 | 63 | rexbidv 3179 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (1st ‘𝑦) → (∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢 ↔ ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢)) |
| 65 | 62, 64 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (1st ‘𝑦) → ((𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) ↔ ((1st
‘𝑦)
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)(1st ‘𝑦) <R
𝑢))) |
| 66 | 65 | rspccv 3619 |
. . . . . . . . . . . . . . 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 240 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → (𝑦 <ℝ
〈𝑣,
0R〉 → (∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢))) |
| 70 | 69 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑦 <ℝ
〈𝑣,
0R〉 → (∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢) → ∃𝑢 ∈ (1st “
𝐴)(1st
‘𝑦)
<R 𝑢))) |
| 71 | | fvelimab 6981 |
. . . . . . . . . . . . . . . 16
⊢
((1st Fn V ∧ 𝐴 ⊆ V) → (𝑢 ∈ (1st “ 𝐴) ↔ ∃𝑧 ∈ 𝐴 (1st ‘𝑧) = 𝑢)) |
| 72 | 7, 8, 71 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (1st “
𝐴) ↔ ∃𝑧 ∈ 𝐴 (1st ‘𝑧) = 𝑢) |
| 73 | | ssel2 3978 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
| 74 | | ltresr2 11181 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 <ℝ 𝑧 ↔ (1st
‘𝑦)
<R (1st ‘𝑧))) |
| 75 | 73, 74 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴)) → (𝑦 <ℝ 𝑧 ↔ (1st ‘𝑦) <R
(1st ‘𝑧))) |
| 76 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑧) = 𝑢 → ((1st ‘𝑦) <R
(1st ‘𝑧)
↔ (1st ‘𝑦) <R 𝑢)) |
| 77 | 75, 76 | sylan9bb 509 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴)) ∧ (1st ‘𝑧) = 𝑢) → (𝑦 <ℝ 𝑧 ↔ (1st ‘𝑦) <R
𝑢)) |
| 78 | 77 | exbiri 811 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ ∧ (𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴)) → ((1st ‘𝑧) = 𝑢 → ((1st ‘𝑦) <R
𝑢 → 𝑦 <ℝ 𝑧))) |
| 79 | 78 | expr 456 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧 ∈ 𝐴 → ((1st ‘𝑧) = 𝑢 → ((1st ‘𝑦) <R
𝑢 → 𝑦 <ℝ 𝑧)))) |
| 80 | 79 | com4r 94 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑦) <R 𝑢 → ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑧 ∈ 𝐴 → ((1st ‘𝑧) = 𝑢 → 𝑦 <ℝ 𝑧)))) |
| 81 | 80 | imp 406 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑧 ∈ 𝐴 → ((1st ‘𝑧) = 𝑢 → 𝑦 <ℝ 𝑧))) |
| 82 | 81 | reximdvai 3165 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (∃𝑧 ∈ 𝐴 (1st ‘𝑧) = 𝑢 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
| 83 | 72, 82 | biimtrid 242 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘𝑦) <R 𝑢 ∧ (𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ)) → (𝑢 ∈ (1st “
𝐴) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) |
| 84 | 83 | expcom 413 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) →
((1st ‘𝑦)
<R 𝑢 → (𝑢 ∈ (1st “ 𝐴) → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
| 85 | 84 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ) → (𝑢 ∈ (1st “
𝐴) → ((1st
‘𝑦)
<R 𝑢 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
| 86 | 85 | rexlimdv 3153 |
. . . . . . . . . . 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 412 |
. . . . . . . 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 3152 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
(∀𝑤 ∈
R (𝑤
<R 𝑣 → ∃𝑢 ∈ (1st “ 𝐴)𝑤 <R 𝑢) → ∀𝑦 ∈ ℝ (𝑦 <ℝ
〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
| 93 | | opelreal 11170 |
. . . . . . . 8
⊢
(〈𝑣,
0R〉 ∈ ℝ ↔ 𝑣 ∈ R) |
| 94 | 93 | biimpri 228 |
. . . . . . 7
⊢ (𝑣 ∈ R →
〈𝑣,
0R〉 ∈ ℝ) |
| 95 | 94 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
〈𝑣,
0R〉 ∈ ℝ) |
| 96 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑣, 0R〉 →
(𝑥 <ℝ
𝑦 ↔ 〈𝑣,
0R〉 <ℝ 𝑦)) |
| 97 | 96 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑣, 0R〉 →
(¬ 𝑥
<ℝ 𝑦
↔ ¬ 〈𝑣,
0R〉 <ℝ 𝑦)) |
| 98 | 97 | ralbidv 3178 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑣, 0R〉 →
(∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦)) |
| 99 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑣, 0R〉 →
(𝑦 <ℝ
𝑥 ↔ 𝑦 <ℝ 〈𝑣,
0R〉)) |
| 100 | 99 | imbi1d 341 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑣, 0R〉 →
((𝑦 <ℝ
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) ↔ (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
| 101 | 100 | ralbidv 3178 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑣, 0R〉 →
(∀𝑦 ∈ ℝ
(𝑦 <ℝ
𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 <ℝ 〈𝑣,
0R〉 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
| 102 | 98, 101 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑣, 0R〉 →
((∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
| 103 | 102 | rspcev 3622 |
. . . . . . 7
⊢
((〈𝑣,
0R〉 ∈ ℝ ∧ (∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |
| 104 | 103 | ex 412 |
. . . . . 6
⊢
(〈𝑣,
0R〉 ∈ ℝ → ((∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
| 105 | 95, 104 | syl 17 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
((∀𝑦 ∈ 𝐴 ¬ 〈𝑣, 0R〉
<ℝ 𝑦
∧ ∀𝑦 ∈
ℝ (𝑦
<ℝ 〈𝑣, 0R〉 →
∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
| 106 | 57, 92, 105 | syl2and 608 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) ∧ 𝑣 ∈ R) →
((∀𝑤 ∈
(1st “ 𝐴)
¬ 𝑣
<R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R 𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
| 107 | 106 | rexlimdva 3155 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑣 ∈
R (∀𝑤
∈ (1st “ 𝐴) ¬ 𝑣 <R 𝑤 ∧ ∀𝑤 ∈ R (𝑤 <R
𝑣 → ∃𝑢 ∈ (1st “
𝐴)𝑤 <R 𝑢)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
| 108 | 32, 42, 107 | 3syld 60 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) →
(∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))) |
| 109 | 108 | 3impia 1118 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) |