Proof of Theorem rnmptbddlem
Step | Hyp | Ref
| Expression |
1 | | rnmptbddlem.b |
. 2
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
2 | | vex 3401 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
3 | | eqid 2778 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
4 | 3 | elrnmpt 5618 |
. . . . . . . . 9
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
5 | 2, 4 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
6 | 5 | biimpi 208 |
. . . . . . 7
⊢ (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
7 | 6 | adantl 475 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
8 | | rnmptbddlem.x |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝜑 |
9 | | nfv 1957 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑦 ∈ ℝ |
10 | 8, 9 | nfan 1946 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ℝ) |
11 | | nfra1 3123 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 |
12 | 10, 11 | nfan 1946 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
13 | | nfv 1957 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑧 ≤ 𝑦 |
14 | | rspa 3112 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑦) |
15 | 14 | 3adant3 1123 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝐵 ≤ 𝑦) |
16 | | simp3 1129 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵) |
17 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝐵 ≤ 𝑦 ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵) |
18 | | simpl 476 |
. . . . . . . . . . . 12
⊢ ((𝐵 ≤ 𝑦 ∧ 𝑧 = 𝐵) → 𝐵 ≤ 𝑦) |
19 | 17, 18 | eqbrtrd 4908 |
. . . . . . . . . . 11
⊢ ((𝐵 ≤ 𝑦 ∧ 𝑧 = 𝐵) → 𝑧 ≤ 𝑦) |
20 | 15, 16, 19 | syl2anc 579 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑧 ≤ 𝑦) |
21 | 20 | 3exp 1109 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑧 ≤ 𝑦))) |
22 | 21 | adantl 475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑧 ≤ 𝑦))) |
23 | 12, 13, 22 | rexlimd 3208 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝑦)) |
24 | 23 | imp 397 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → 𝑧 ≤ 𝑦) |
25 | 7, 24 | syldan 585 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑧 ≤ 𝑦) |
26 | 25 | ralrimiva 3148 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |
27 | 26 | ex 403 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) |
28 | 27 | reximdva 3198 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) |
29 | 1, 28 | mpd 15 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) |