Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
2 | 1 | elrnmpt 5867 |
. . . . . 6
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
3 | 2 | elv 3437 |
. . . . 5
⊢ (𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
4 | | nfra1 3144 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 |
5 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑤 ≤ 𝑧 |
6 | | rspa 3132 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑤 ≤ 𝐵) |
7 | 6 | 3adant3 1131 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑤 ≤ 𝐵) |
8 | | simp3 1137 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵) |
9 | 7, 8 | breqtrrd 5104 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑤 ≤ 𝑧) |
10 | 9 | 3exp 1118 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑤 ≤ 𝑧))) |
11 | 4, 5, 10 | rexlimd 3249 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ≤ 𝑧)) |
12 | 11 | imp 407 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 𝑤 ≤ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → 𝑤 ≤ 𝑧) |
13 | 12 | adantll 711 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵) ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → 𝑤 ≤ 𝑧) |
14 | 3, 13 | sylan2b 594 |
. . . 4
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵) ∧ 𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑤 ≤ 𝑧) |
15 | 14 | ralrimiva 3103 |
. . 3
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵) → ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑤 ≤ 𝑧) |
16 | | rnmptlb.1 |
. . . 4
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) |
17 | | breq1 5079 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑦 ≤ 𝐵 ↔ 𝑤 ≤ 𝐵)) |
18 | 17 | ralbidv 3119 |
. . . . 5
⊢ (𝑦 = 𝑤 → (∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵)) |
19 | 18 | cbvrexvw 3383 |
. . . 4
⊢
(∃𝑦 ∈
ℝ ∀𝑥 ∈
𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵) |
20 | 16, 19 | sylib 217 |
. . 3
⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑤 ≤ 𝐵) |
21 | 15, 20 | reximddv3 42670 |
. 2
⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑤 ≤ 𝑧) |
22 | | breq1 5079 |
. . . 4
⊢ (𝑤 = 𝑦 → (𝑤 ≤ 𝑧 ↔ 𝑦 ≤ 𝑧)) |
23 | 22 | ralbidv 3119 |
. . 3
⊢ (𝑤 = 𝑦 → (∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑤 ≤ 𝑧 ↔ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) |
24 | 23 | cbvrexvw 3383 |
. 2
⊢
(∃𝑤 ∈
ℝ ∀𝑧 ∈
ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑤 ≤ 𝑧 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) |
25 | 21, 24 | sylib 217 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) |