Proof of Theorem infxr
| Step | Hyp | Ref
| Expression |
| 1 | | infxr.b |
. 2
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 2 | | infxr.n |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵) |
| 3 | | infxr.x |
. . 3
⊢
Ⅎ𝑥𝜑 |
| 4 | | infxr.e |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 5 | 4 | r19.21bi 3251 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 6 | 5 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 ∈ ℝ) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 7 | | simplll 775 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬
𝑥 ∈ ℝ) ∧
𝐵 < 𝑥) → 𝜑) |
| 8 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬
𝑥 ∈ ℝ) ∧
𝐵 < 𝑥) → 𝑥 ∈ ℝ*) |
| 9 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬
𝑥 ∈ ℝ) ∧
𝐵 < 𝑥) → ¬ 𝑥 ∈ ℝ) |
| 10 | | mnfxr 11318 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
| 11 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → -∞ ∈
ℝ*) |
| 12 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*) |
| 13 | 1 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝐵 ∈
ℝ*) |
| 14 | | mnfle 13177 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ*
→ -∞ ≤ 𝐵) |
| 15 | 1, 14 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → -∞ ≤ 𝐵) |
| 16 | 15 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → -∞ ≤ 𝐵) |
| 17 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥) |
| 18 | 11, 13, 12, 16, 17 | xrlelttrd 13202 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → -∞ < 𝑥) |
| 19 | 11, 12, 18 | xrgtned 45333 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝐵 < 𝑥) → 𝑥 ≠ -∞) |
| 20 | 19 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬
𝑥 ∈ ℝ) ∧
𝐵 < 𝑥) → 𝑥 ≠ -∞) |
| 21 | 8, 9, 20 | xrnmnfpnf 45088 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬
𝑥 ∈ ℝ) ∧
𝐵 < 𝑥) → 𝑥 = +∞) |
| 22 | | simpr 484 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬
𝑥 ∈ ℝ) ∧
𝐵 < 𝑥) → 𝐵 < 𝑥) |
| 23 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝜑) |
| 24 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = -∞ → 𝐵 = -∞) |
| 25 | | 1re 11261 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
| 26 | | mnflt 13165 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℝ → -∞ < 1) |
| 27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ -∞
< 1 |
| 28 | 24, 27 | eqbrtrdi 5182 |
. . . . . . . . . . . . 13
⊢ (𝐵 = -∞ → 𝐵 < 1) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 = -∞) → 𝐵 < 1) |
| 30 | | 1red 11262 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℝ) |
| 31 | | breq2 5147 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 1 → (𝐵 < 𝑥 ↔ 𝐵 < 1)) |
| 32 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → (𝑦 < 𝑥 ↔ 𝑦 < 1)) |
| 33 | 32 | rexbidv 3179 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 1 → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < 1)) |
| 34 | 31, 33 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1))) |
| 35 | 34 | rspcva 3620 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1)) |
| 36 | 30, 4, 35 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 1)) |
| 37 | 23, 29, 36 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 1) |
| 38 | 37 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 1) |
| 39 | | infxr.y |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝜑 |
| 40 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦 𝑥 = +∞ |
| 41 | 39, 40 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 = +∞) |
| 42 | | infxr.a |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
| 43 | 42 | sselda 3983 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
| 44 | 43 | ad4ant13 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 ∈ ℝ*) |
| 45 | | 1xr 11320 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ* |
| 46 | 45 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 ∈
ℝ*) |
| 47 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = +∞ → 𝑥 = +∞) |
| 48 | | pnfxr 11315 |
. . . . . . . . . . . . . . . . . 18
⊢ +∞
∈ ℝ* |
| 49 | 47, 48 | eqeltrdi 2849 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = +∞ → 𝑥 ∈
ℝ*) |
| 50 | 49 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = +∞) → 𝑥 ∈ ℝ*) |
| 51 | 50 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑥 ∈ ℝ*) |
| 52 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 1) |
| 53 | | ltpnf 13162 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
ℝ → 1 < +∞) |
| 54 | 25, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 <
+∞ |
| 55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = +∞ → 1 <
+∞) |
| 56 | 47 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = +∞ → +∞ =
𝑥) |
| 57 | 55, 56 | breqtrd 5169 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = +∞ → 1 < 𝑥) |
| 58 | 57 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 = +∞) → 1 < 𝑥) |
| 59 | 58 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 1 < 𝑥) |
| 60 | 44, 46, 51, 52, 59 | xrlttrd 13201 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < 1) → 𝑦 < 𝑥) |
| 61 | 60 | ex 412 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < 1 → 𝑦 < 𝑥)) |
| 62 | 61 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = +∞) → (𝑦 ∈ 𝐴 → (𝑦 < 1 → 𝑦 < 𝑥))) |
| 63 | 41, 62 | reximdai 3261 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = +∞) → (∃𝑦 ∈ 𝐴 𝑦 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 64 | 63 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝐵 = -∞) → (∃𝑦 ∈ 𝐴 𝑦 < 1 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 65 | 38, 64 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 = +∞) ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) |
| 66 | 65 | 3adantl3 1169 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) |
| 67 | 1 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐵 = -∞) → 𝐵 ∈
ℝ*) |
| 68 | 67 | 3ad2antl1 1186 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈
ℝ*) |
| 69 | 24 | necon3bi 2967 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐵 = -∞ → 𝐵 ≠ -∞) |
| 70 | 69 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ -∞) |
| 71 | 48 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ ∈
ℝ*) |
| 72 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < 𝑥) |
| 73 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 = +∞) |
| 74 | 72, 73 | breqtrd 5169 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞) |
| 75 | 74 | 3adant1 1131 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝐵 < +∞) |
| 76 | 75 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < +∞) |
| 77 | 68, 71, 76 | xrltned 45368 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ≠ +∞) |
| 78 | 68, 70, 77 | xrred 45376 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 ∈ ℝ) |
| 79 | 25 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 1 ∈
ℝ) |
| 80 | 78, 79 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) ∈ ℝ) |
| 81 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 82 | 81 | 3ad2antl1 1186 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 83 | 80, 82 | jca 511 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ((𝐵 + 1) ∈ ℝ ∧ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))) |
| 84 | 78 | ltp1d 12198 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → 𝐵 < (𝐵 + 1)) |
| 85 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐵 + 1) → (𝐵 < 𝑥 ↔ 𝐵 < (𝐵 + 1))) |
| 86 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐵 + 1) → (𝑦 < 𝑥 ↔ 𝑦 < (𝐵 + 1))) |
| 87 | 86 | rexbidv 3179 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐵 + 1) → (∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1))) |
| 88 | 85, 87 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐵 + 1) → ((𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) ↔ (𝐵 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1)))) |
| 89 | 88 | rspcva 3620 |
. . . . . . . . . 10
⊢ (((𝐵 + 1) ∈ ℝ ∧
∀𝑥 ∈ ℝ
(𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → (𝐵 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1))) |
| 90 | 83, 84, 89 | sylc 65 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1)) |
| 91 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝐵 < 𝑥 |
| 92 | 39, 40, 91 | nf3an 1901 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) |
| 93 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 ¬ 𝐵 = -∞ |
| 94 | 92, 93 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑦((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) |
| 95 | 43 | 3ad2antl1 1186 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
| 96 | 95 | ad4ant13 751 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 ∈ ℝ*) |
| 97 | 80 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝐵 + 1) ∈ ℝ) |
| 98 | 97 | rexrd 11311 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝐵 + 1) ∈
ℝ*) |
| 99 | 98 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) ∈
ℝ*) |
| 100 | 50 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → 𝑥 ∈ ℝ*) |
| 101 | 100 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑥 ∈ ℝ*) |
| 102 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < (𝐵 + 1)) |
| 103 | 80 | ltpnfd 13163 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < +∞) |
| 104 | 56 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = +∞ ∧ ¬ 𝐵 = -∞) → +∞ =
𝑥) |
| 105 | 104 | 3ad2antl2 1187 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → +∞ = 𝑥) |
| 106 | 103, 105 | breqtrd 5169 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝐵 + 1) < 𝑥) |
| 107 | 106 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → (𝐵 + 1) < 𝑥) |
| 108 | 96, 99, 101, 102, 107 | xrlttrd 13201 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 < (𝐵 + 1)) → 𝑦 < 𝑥) |
| 109 | 108 | ex 412 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) ∧ 𝑦 ∈ 𝐴) → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥)) |
| 110 | 109 | ex 412 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (𝑦 ∈ 𝐴 → (𝑦 < (𝐵 + 1) → 𝑦 < 𝑥))) |
| 111 | 94, 110 | reximdai 3261 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → (∃𝑦 ∈ 𝐴 𝑦 < (𝐵 + 1) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 112 | 90, 111 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) ∧ ¬ 𝐵 = -∞) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) |
| 113 | 66, 112 | pm2.61dan 813 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = +∞ ∧ 𝐵 < 𝑥) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) |
| 114 | 7, 21, 22, 113 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬
𝑥 ∈ ℝ) ∧
𝐵 < 𝑥) → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥) |
| 115 | 114 | ex 412 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬
𝑥 ∈ ℝ) →
(𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 116 | 6, 115 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 117 | 116 | ex 412 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ* → (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥))) |
| 118 | 3, 117 | ralrimi 3257 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) |
| 119 | | xrltso 13183 |
. . . . 5
⊢ < Or
ℝ* |
| 120 | 119 | a1i 11 |
. . . 4
⊢ (⊤
→ < Or ℝ*) |
| 121 | 120 | eqinf 9524 |
. . 3
⊢ (⊤
→ ((𝐵 ∈
ℝ* ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ*, < ) = 𝐵)) |
| 122 | 121 | mptru 1547 |
. 2
⊢ ((𝐵 ∈ ℝ*
∧ ∀𝑥 ∈
𝐴 ¬ 𝑥 < 𝐵 ∧ ∀𝑥 ∈ ℝ* (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) → inf(𝐴, ℝ*, < ) = 𝐵) |
| 123 | 1, 2, 118, 122 | syl3anc 1373 |
1
⊢ (𝜑 → inf(𝐴, ℝ*, < ) = 𝐵) |