| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 2 | 1 | elrnmpt 5969 |
. . . . . 6
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
| 3 | 2 | elv 3485 |
. . . . 5
⊢ (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
| 4 | | nfra1 3284 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 |
| 5 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑤 ≤ 𝑧 |
| 6 | | rspa 3248 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑤 ≤ 𝐵) |
| 7 | 6 | 3adant3 1133 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑤 ≤ 𝐵) |
| 8 | | simp3 1139 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵) |
| 9 | 7, 8 | breqtrrd 5171 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑤 ≤ 𝑧) |
| 10 | 9 | 3exp 1120 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ≤ 𝑧))) |
| 11 | 4, 5, 10 | rexlimd 3266 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ≤ 𝑧)) |
| 12 | 11 | imp 406 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → 𝑤 ≤ 𝑧) |
| 13 | 12 | adantll 714 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵) ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → 𝑤 ≤ 𝑧) |
| 14 | 3, 13 | sylan2b 594 |
. . . 4
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵) ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑤 ≤ 𝑧) |
| 15 | 14 | ralrimiva 3146 |
. . 3
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑤 ≤ 𝑧) |
| 16 | | rnmptlb.1 |
. . . 4
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) |
| 17 | | breq1 5146 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑦 ≤ 𝐵 ↔ 𝑤 ≤ 𝐵)) |
| 18 | 17 | ralbidv 3178 |
. . . . 5
⊢ (𝑦 = 𝑤 → (∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵)) |
| 19 | 18 | cbvrexvw 3238 |
. . . 4
⊢
(∃𝑦 ∈
ℝ ∀𝑥 ∈
𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵) |
| 20 | 16, 19 | sylib 218 |
. . 3
⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵) |
| 21 | 15, 20 | reximddv3 3172 |
. 2
⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑤 ≤ 𝑧) |
| 22 | | breq1 5146 |
. . . 4
⊢ (𝑤 = 𝑦 → (𝑤 ≤ 𝑧 ↔ 𝑦 ≤ 𝑧)) |
| 23 | 22 | ralbidv 3178 |
. . 3
⊢ (𝑤 = 𝑦 → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑤 ≤ 𝑧 ↔ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) |
| 24 | 23 | cbvrexvw 3238 |
. 2
⊢
(∃𝑤 ∈
ℝ ∀𝑧 ∈
ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑤 ≤ 𝑧 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) |
| 25 | 21, 24 | sylib 218 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) |