Proof of Theorem rnmptbdlem
Step | Hyp | Ref
| Expression |
1 | | rnmptbdlem.x |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
2 | | nfcv 2979 |
. . . . . 6
⊢
Ⅎ𝑥ℝ |
3 | | nfra1 3221 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 |
4 | 2, 3 | nfrex 3311 |
. . . . 5
⊢
Ⅎ𝑥∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 |
5 | 1, 4 | nfan 1900 |
. . . 4
⊢
Ⅎ𝑥(𝜑 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
6 | | simpr 487 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
7 | 5, 6 | rnmptbdd 41523 |
. . 3
⊢ ((𝜑 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |
8 | 7 | ex 415 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) |
9 | | rnmptbdlem.y |
. . 3
⊢
Ⅎ𝑦𝜑 |
10 | | nfmpt1 5166 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
11 | 10 | nfrn 5826 |
. . . . . . . 8
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
12 | | nfv 1915 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑧 ≤ 𝑦 |
13 | 11, 12 | nfralw 3227 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 |
14 | 1, 13 | nfan 1900 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |
15 | | breq1 5071 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
16 | | simplr 767 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |
17 | | eqid 2823 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
18 | | simpr 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
19 | | rnmptbdlem.b |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
20 | 19 | adantlr 713 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
21 | 17, 18, 20 | elrnmpt1d 41507 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
22 | 15, 16, 21 | rspcdva 3627 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑦) |
23 | 14, 22 | ralrimia 41405 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
24 | 23 | ex 415 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)) |
25 | 24 | a1d 25 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦))) |
26 | 9, 25 | reximdai 3313 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)) |
27 | 8, 26 | impbid 214 |
1
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) |