Step | Hyp | Ref
| Expression |
1 | | sge0supre.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
2 | | sge0supre.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
3 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝑋 ∈ 𝑉) |
4 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,]+∞)) |
5 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐹) |
6 | 3, 4, 5 | sge0pnfval 40590 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = +∞) |
7 | | sge0supre.re |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘𝐹) ∈ ℝ) |
8 | 1, 2 | sge0repnf 40603 |
. . . . . . 7
⊢ (𝜑 →
((Σ^‘𝐹) ∈ ℝ ↔ ¬
(Σ^‘𝐹) = +∞)) |
9 | 7, 8 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → ¬
(Σ^‘𝐹) = +∞) |
10 | 9 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ¬
(Σ^‘𝐹) = +∞) |
11 | 6, 10 | pm2.65da 600 |
. . . 4
⊢ (𝜑 → ¬ +∞ ∈ ran
𝐹) |
12 | 2, 11 | fge0iccico 40587 |
. . 3
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) |
13 | 1, 12 | sge0reval 40589 |
. 2
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
14 | 12 | sge0rnre 40581 |
. . 3
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ) |
15 | | sge0rnn0 40585 |
. . . 4
⊢ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅ |
16 | 15 | a1i 11 |
. . 3
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅) |
17 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
18 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
19 | 18 | elrnmpt 5372 |
. . . . . . . 8
⊢ (𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
20 | 19 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → (𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
21 | 17, 20 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
22 | | simp3 1063 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
23 | | ressxr 10083 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
⊆ ℝ* |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℝ ⊆
ℝ*) |
25 | 14, 24 | sstrd 3613 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆
ℝ*) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆
ℝ*) |
27 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) |
28 | | sumex 14418 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑦 ∈
𝑥 (𝐹‘𝑦) ∈ V |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ V) |
30 | 18 | elrnmpt1 5374 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ V) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
31 | 27, 29, 30 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
33 | | supxrub 12154 |
. . . . . . . . . . . . 13
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ* ∧
Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
34 | 26, 32, 33 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
35 | 13 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) =
(Σ^‘𝐹)) |
36 | 35 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) =
(Σ^‘𝐹)) |
37 | 34, 36 | breqtrd 4679 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤
(Σ^‘𝐹)) |
38 | 37 | 3adant3 1081 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤
(Σ^‘𝐹)) |
39 | 22, 38 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑤 ≤
(Σ^‘𝐹)) |
40 | 39 | 3exp 1264 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → (𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑤 ≤
(Σ^‘𝐹)))) |
41 | 40 | rexlimdv 3030 |
. . . . . . 7
⊢ (𝜑 → (∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑤 ≤
(Σ^‘𝐹))) |
42 | 41 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → (∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑤 ≤
(Σ^‘𝐹))) |
43 | 21, 42 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → 𝑤 ≤
(Σ^‘𝐹)) |
44 | 43 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤
(Σ^‘𝐹)) |
45 | | breq2 4657 |
. . . . . 6
⊢ (𝑧 =
(Σ^‘𝐹) → (𝑤 ≤ 𝑧 ↔ 𝑤 ≤
(Σ^‘𝐹))) |
46 | 45 | ralbidv 2986 |
. . . . 5
⊢ (𝑧 =
(Σ^‘𝐹) → (∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤ 𝑧 ↔ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤
(Σ^‘𝐹))) |
47 | 46 | rspcev 3309 |
. . . 4
⊢
(((Σ^‘𝐹) ∈ ℝ ∧ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤
(Σ^‘𝐹)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤ 𝑧) |
48 | 7, 44, 47 | syl2anc 693 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤ 𝑧) |
49 | | supxrre 12157 |
. . 3
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤ 𝑧) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )) |
50 | 14, 16, 48, 49 | syl3anc 1326 |
. 2
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )) |
51 | 13, 50 | eqtrd 2656 |
1
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )) |