Proof of Theorem xrinfmexpnf
Step | Hyp | Ref
| Expression |
1 | | elun 4039 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴 ∪ {+∞}) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ {+∞})) |
2 | | simpr 488 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) |
3 | | velsn 4532 |
. . . . . . . . 9
⊢ (𝑦 ∈ {+∞} ↔ 𝑦 = +∞) |
4 | | pnfnlt 12606 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
→ ¬ +∞ < 𝑥) |
5 | | breq1 5033 |
. . . . . . . . . . 11
⊢ (𝑦 = +∞ → (𝑦 < 𝑥 ↔ +∞ < 𝑥)) |
6 | 5 | notbid 321 |
. . . . . . . . . 10
⊢ (𝑦 = +∞ → (¬ 𝑦 < 𝑥 ↔ ¬ +∞ < 𝑥)) |
7 | 4, 6 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
→ (𝑦 = +∞ →
¬ 𝑦 < 𝑥)) |
8 | 3, 7 | syl5bi 245 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ {+∞}
→ ¬ 𝑦 < 𝑥)) |
9 | 8 | adantr 484 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → (𝑦 ∈ {+∞} → ¬ 𝑦 < 𝑥)) |
10 | 2, 9 | jaod 858 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → ((𝑦 ∈ 𝐴 ∨ 𝑦 ∈ {+∞}) → ¬ 𝑦 < 𝑥)) |
11 | 1, 10 | syl5bi 245 |
. . . . 5
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → (𝑦 ∈ (𝐴 ∪ {+∞}) → ¬ 𝑦 < 𝑥)) |
12 | 11 | ex 416 |
. . . 4
⊢ (𝑥 ∈ ℝ*
→ ((𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥) → (𝑦 ∈ (𝐴 ∪ {+∞}) → ¬ 𝑦 < 𝑥))) |
13 | 12 | ralimdv2 3090 |
. . 3
⊢ (𝑥 ∈ ℝ*
→ (∀𝑦 ∈
𝐴 ¬ 𝑦 < 𝑥 → ∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥)) |
14 | | elun1 4066 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ (𝐴 ∪ {+∞})) |
15 | 14 | anim1i 618 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑧 < 𝑦) → (𝑧 ∈ (𝐴 ∪ {+∞}) ∧ 𝑧 < 𝑦)) |
16 | 15 | reximi2 3158 |
. . . . 5
⊢
(∃𝑧 ∈
𝐴 𝑧 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦) |
17 | 16 | imim2i 16 |
. . . 4
⊢ ((𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)) |
18 | 17 | ralimi 3075 |
. . 3
⊢
(∀𝑦 ∈
ℝ* (𝑥 <
𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)) |
19 | 13, 18 | anim12d1 613 |
. 2
⊢ (𝑥 ∈ ℝ*
→ ((∀𝑦 ∈
𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)))) |
20 | 19 | reximia 3156 |
1
⊢
(∃𝑥 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦))) |