Proof of Theorem rnmptbdlem
| Step | Hyp | Ref
| Expression |
| 1 | | rnmptbdlem.x |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
| 2 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥ℝ |
| 3 | | nfra1 3284 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 |
| 4 | 2, 3 | nfrexw 3313 |
. . . . 5
⊢
Ⅎ𝑥∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 |
| 5 | 1, 4 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑥(𝜑 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
| 6 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
| 7 | 5, 6 | rnmptbdd 45252 |
. . 3
⊢ ((𝜑 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |
| 8 | 7 | ex 412 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) |
| 9 | | rnmptbdlem.y |
. . 3
⊢
Ⅎ𝑦𝜑 |
| 10 | | nfmpt1 5250 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 11 | 10 | nfrn 5963 |
. . . . . . . 8
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 12 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑧 ≤ 𝑦 |
| 13 | 11, 12 | nfralw 3311 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 |
| 14 | 1, 13 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |
| 15 | | breq1 5146 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
| 16 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |
| 17 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 18 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 19 | | rnmptbdlem.b |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
| 20 | 19 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
| 21 | 17, 18, 20 | elrnmpt1d 5975 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 22 | 15, 16, 21 | rspcdva 3623 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑦) |
| 23 | 14, 22 | ralrimia 3258 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
| 24 | 23 | ex 412 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)) |
| 25 | 24 | a1d 25 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦))) |
| 26 | 9, 25 | reximdai 3261 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)) |
| 27 | 8, 26 | impbid 212 |
1
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) |