Proof of Theorem xrinfmexpnf
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elun 4153 | . . . . . 6
⊢ (𝑦 ∈ (𝐴 ∪ {+∞}) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ {+∞})) | 
| 2 |  | simpr 484 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) | 
| 3 |  | velsn 4642 | . . . . . . . . 9
⊢ (𝑦 ∈ {+∞} ↔ 𝑦 = +∞) | 
| 4 |  | pnfnlt 13170 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
→ ¬ +∞ < 𝑥) | 
| 5 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑦 = +∞ → (𝑦 < 𝑥 ↔ +∞ < 𝑥)) | 
| 6 | 5 | notbid 318 | . . . . . . . . . 10
⊢ (𝑦 = +∞ → (¬ 𝑦 < 𝑥 ↔ ¬ +∞ < 𝑥)) | 
| 7 | 4, 6 | syl5ibrcom 247 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
→ (𝑦 = +∞ →
¬ 𝑦 < 𝑥)) | 
| 8 | 3, 7 | biimtrid 242 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ*
→ (𝑦 ∈ {+∞}
→ ¬ 𝑦 < 𝑥)) | 
| 9 | 8 | adantr 480 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → (𝑦 ∈ {+∞} → ¬ 𝑦 < 𝑥)) | 
| 10 | 2, 9 | jaod 860 | . . . . . 6
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → ((𝑦 ∈ 𝐴 ∨ 𝑦 ∈ {+∞}) → ¬ 𝑦 < 𝑥)) | 
| 11 | 1, 10 | biimtrid 242 | . . . . 5
⊢ ((𝑥 ∈ ℝ*
∧ (𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥)) → (𝑦 ∈ (𝐴 ∪ {+∞}) → ¬ 𝑦 < 𝑥)) | 
| 12 | 11 | ex 412 | . . . 4
⊢ (𝑥 ∈ ℝ*
→ ((𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥) → (𝑦 ∈ (𝐴 ∪ {+∞}) → ¬ 𝑦 < 𝑥))) | 
| 13 | 12 | ralimdv2 3163 | . . 3
⊢ (𝑥 ∈ ℝ*
→ (∀𝑦 ∈
𝐴 ¬ 𝑦 < 𝑥 → ∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥)) | 
| 14 |  | elun1 4182 | . . . . . . 7
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ (𝐴 ∪ {+∞})) | 
| 15 | 14 | anim1i 615 | . . . . . 6
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑧 < 𝑦) → (𝑧 ∈ (𝐴 ∪ {+∞}) ∧ 𝑧 < 𝑦)) | 
| 16 | 15 | reximi2 3079 | . . . . 5
⊢
(∃𝑧 ∈
𝐴 𝑧 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦) | 
| 17 | 16 | imim2i 16 | . . . 4
⊢ ((𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)) | 
| 18 | 17 | ralimi 3083 | . . 3
⊢
(∀𝑦 ∈
ℝ* (𝑥 <
𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) → ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)) | 
| 19 | 13, 18 | anim12d1 610 | . 2
⊢ (𝑥 ∈ ℝ*
→ ((∀𝑦 ∈
𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)))) | 
| 20 | 19 | reximia 3081 | 1
⊢
(∃𝑥 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦))) |