Proof of Theorem xrinfmexpnf
Step | Hyp | Ref
| Expression |
1 | | elun 4083 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴 ∪ {+∞}) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ {+∞})) |
2 | | simpr 485 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) |
3 | | velsn 4577 |
. . . . . . . . 9
⊢ (𝑦 ∈ {+∞} ↔ 𝑦 = +∞) |
4 | | pnfnlt 12864 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
→ ¬ +∞ < 𝑥) |
5 | | breq1 5077 |
. . . . . . . . . . 11
⊢ (𝑦 = +∞ → (𝑦 < 𝑥 ↔ +∞ < 𝑥)) |
6 | 5 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑦 = +∞ → (¬ 𝑦 < 𝑥 ↔ ¬ +∞ < 𝑥)) |
7 | 4, 6 | syl5ibrcom 246 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
→ (𝑦 = +∞ →
¬ 𝑦 < 𝑥)) |
8 | 3, 7 | syl5bi 241 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ {+∞}
→ ¬ 𝑦 < 𝑥)) |
9 | 8 | adantr 481 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → (𝑦 ∈ {+∞} → ¬ 𝑦 < 𝑥)) |
10 | 2, 9 | jaod 856 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → ((𝑦 ∈ 𝐴 ∨ 𝑦 ∈ {+∞}) → ¬ 𝑦 < 𝑥)) |
11 | 1, 10 | syl5bi 241 |
. . . . 5
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → (𝑦 ∈ (𝐴 ∪ {+∞}) → ¬ 𝑦 < 𝑥)) |
12 | 11 | ex 413 |
. . . 4
⊢ (𝑥 ∈ ℝ*
→ ((𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥) → (𝑦 ∈ (𝐴 ∪ {+∞}) → ¬ 𝑦 < 𝑥))) |
13 | 12 | ralimdv2 3107 |
. . 3
⊢ (𝑥 ∈ ℝ*
→ (∀𝑦 ∈
𝐴 ¬ 𝑦 < 𝑥 → ∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥)) |
14 | | elun1 4110 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ (𝐴 ∪ {+∞})) |
15 | 14 | anim1i 615 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑧 < 𝑦) → (𝑧 ∈ (𝐴 ∪ {+∞}) ∧ 𝑧 < 𝑦)) |
16 | 15 | reximi2 3175 |
. . . . 5
⊢
(∃𝑧 ∈
𝐴 𝑧 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦) |
17 | 16 | imim2i 16 |
. . . 4
⊢ ((𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)) |
18 | 17 | ralimi 3087 |
. . 3
⊢
(∀𝑦 ∈
ℝ* (𝑥 <
𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)) |
19 | 13, 18 | anim12d1 610 |
. 2
⊢ (𝑥 ∈ ℝ*
→ ((∀𝑦 ∈
𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)))) |
20 | 19 | reximia 3176 |
1
⊢
(∃𝑥 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦))) |