Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . 3
⊢
Ⅎ𝑥𝜑 |
2 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑧 ∈ (𝒫 𝑋 ∩ Fin)) |
3 | | sge0gerp.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
4 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞)) |
5 | | elinel1 3761 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝒫 𝑋 ∩ Fin) → 𝑧 ∈ 𝒫 𝑋) |
6 | | elpwi 4117 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝒫 𝑋 → 𝑧 ⊆ 𝑋) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝒫 𝑋 ∩ Fin) → 𝑧 ⊆ 𝑋) |
8 | 7 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑧 ⊆ 𝑋) |
9 | 4, 8 | fssresd 5984 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞)) |
10 | 2, 9 | sge0xrcl 39278 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑧)) ∈
ℝ*) |
11 | 10 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑧)) ∈
ℝ*) |
12 | | eqid 2610 |
. . . . 5
⊢ (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧))) = (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧))) |
13 | 12 | rnmptss 6299 |
. . . 4
⊢
(∀𝑧 ∈
(𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑧)) ∈ ℝ* → ran
(𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧))) ⊆
ℝ*) |
14 | 11, 13 | syl 17 |
. . 3
⊢ (𝜑 → ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧))) ⊆
ℝ*) |
15 | | sge0gerp.a |
. . 3
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
16 | | sge0gerp.z |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑧 ∈ (𝒫
𝑋 ∩ Fin)𝐴 ≤
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥)) |
17 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑧(𝜑 ∧ 𝑥 ∈ ℝ+) |
18 | | nfmpt1 4675 |
. . . . . . 7
⊢
Ⅎ𝑧(𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧))) |
19 | 18 | nfrn 5289 |
. . . . . 6
⊢
Ⅎ𝑧ran
(𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧))) |
20 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑧 𝐴 ≤ (𝑦 +𝑒 𝑥) |
21 | 19, 20 | nfrex 2990 |
. . . . 5
⊢
Ⅎ𝑧∃𝑦 ∈ ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧)))𝐴 ≤ (𝑦 +𝑒 𝑥) |
22 | | id 22 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝒫 𝑋 ∩ Fin) → 𝑧 ∈ (𝒫 𝑋 ∩ Fin)) |
23 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Σ^‘(𝐹 ↾ 𝑧)) ∈ V |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝒫 𝑋 ∩ Fin) →
(Σ^‘(𝐹 ↾ 𝑧)) ∈ V) |
25 | 12 | elrnmpt1 5295 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (𝒫 𝑋 ∩ Fin) ∧
(Σ^‘(𝐹 ↾ 𝑧)) ∈ V) →
(Σ^‘(𝐹 ↾ 𝑧)) ∈ ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧)))) |
26 | 22, 24, 25 | syl2anc 691 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝒫 𝑋 ∩ Fin) →
(Σ^‘(𝐹 ↾ 𝑧)) ∈ ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧)))) |
27 | 26 | 3ad2ant2 1076 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑧 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝐴 ≤
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥)) →
(Σ^‘(𝐹 ↾ 𝑧)) ∈ ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧)))) |
28 | | simp3 1056 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑧 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝐴 ≤
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥)) → 𝐴 ≤
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥)) |
29 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝐴 ≤
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥) |
30 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑦 =
(Σ^‘(𝐹 ↾ 𝑧)) → (𝑦 +𝑒 𝑥) =
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥)) |
31 | 30 | breq2d 4595 |
. . . . . . . 8
⊢ (𝑦 =
(Σ^‘(𝐹 ↾ 𝑧)) → (𝐴 ≤ (𝑦 +𝑒 𝑥) ↔ 𝐴 ≤
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥))) |
32 | 29, 31 | rspce 3277 |
. . . . . . 7
⊢
(((Σ^‘(𝐹 ↾ 𝑧)) ∈ ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧))) ∧ 𝐴 ≤
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥)) → ∃𝑦 ∈ ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧)))𝐴 ≤ (𝑦 +𝑒 𝑥)) |
33 | 27, 28, 32 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑧 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝐴 ≤
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥)) → ∃𝑦 ∈ ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧)))𝐴 ≤ (𝑦 +𝑒 𝑥)) |
34 | 33 | 3exp 1256 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑧 ∈ (𝒫 𝑋 ∩ Fin) → (𝐴 ≤
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥) → ∃𝑦 ∈ ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧)))𝐴 ≤ (𝑦 +𝑒 𝑥)))) |
35 | 17, 21, 34 | rexlimd 3008 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑧 ∈ (𝒫
𝑋 ∩ Fin)𝐴 ≤
((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥) → ∃𝑦 ∈ ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧)))𝐴 ≤ (𝑦 +𝑒 𝑥))) |
36 | 16, 35 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧)))𝐴 ≤ (𝑦 +𝑒 𝑥)) |
37 | 1, 14, 15, 36 | supxrge 38495 |
. 2
⊢ (𝜑 → 𝐴 ≤ sup(ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧))), ℝ*, <
)) |
38 | | sge0gerp.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
39 | 38, 3 | sge0sup 39284 |
. . 3
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧))), ℝ*, <
)) |
40 | 39 | eqcomd 2616 |
. 2
⊢ (𝜑 → sup(ran (𝑧 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑧))), ℝ*, < ) =
(Σ^‘𝐹)) |
41 | 37, 40 | breqtrd 4609 |
1
⊢ (𝜑 → 𝐴 ≤
(Σ^‘𝐹)) |