Proof of Theorem rnmptbdlem
Step | Hyp | Ref
| Expression |
1 | | rnmptbdlem.x |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
2 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑥ℝ |
3 | | nfra1 2941 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 |
4 | 2, 3 | nfrex 3007 |
. . . . 5
⊢
Ⅎ𝑥∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 |
5 | 1, 4 | nfan 1828 |
. . . 4
⊢
Ⅎ𝑥(𝜑 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
6 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
7 | 5, 6 | rnmptbdd 39456 |
. . 3
⊢ ((𝜑 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |
8 | 7 | ex 450 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) |
9 | | rnmptbdlem.y |
. . 3
⊢
Ⅎ𝑦𝜑 |
10 | | nfmpt1 4747 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
11 | 10 | nfrn 5368 |
. . . . . . . 8
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
12 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑧 ≤ 𝑦 |
13 | 11, 12 | nfral 2945 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 |
14 | 1, 13 | nfan 1828 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |
15 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
16 | | rnmptbdlem.b |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
17 | 16 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
18 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
19 | 18 | elrnmpt1 5374 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
20 | 15, 17, 19 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
21 | | simplr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |
22 | | breq1 4656 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → (𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦)) |
23 | 22 | rspcva 3307 |
. . . . . . . 8
⊢ ((𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) → 𝐵 ≤ 𝑦) |
24 | 20, 21, 23 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑦) |
25 | 24 | ex 450 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) → (𝑥 ∈ 𝐴 → 𝐵 ≤ 𝑦)) |
26 | 14, 25 | ralrimi 2957 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
27 | 26 | ex 450 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)) |
28 | 27 | a1d 25 |
. . 3
⊢ (𝜑 → (𝑦 ∈ ℝ → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦))) |
29 | 9, 28 | reximdai 3012 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)) |
30 | 8, 29 | impbid 202 |
1
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) |