Step | Hyp | Ref
| Expression |
1 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ =
+∞) |
2 | | sge0sup.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
3 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝑋 ∈ 𝑉) |
4 | | sge0sup.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
5 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,]+∞)) |
6 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐹) |
7 | 3, 5, 6 | sge0pnfval 39266 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = +∞) |
8 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
9 | 8 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ V) |
10 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞)) |
11 | | elinel1 3761 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ 𝒫 𝑋) |
12 | | elpwi 4117 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋) |
14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋) |
15 | 10, 14 | fssresd 5984 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
16 | 9, 15 | sge0xrcl 39278 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) |
17 | 16 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) |
18 | 17 | ralrimiva 2949 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) |
19 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) |
20 | 19 | rnmptss 6299 |
. . . . 5
⊢
(∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆
ℝ*) |
21 | 18, 20 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆
ℝ*) |
22 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐹:𝑋⟶(0[,]+∞) → 𝐹 Fn 𝑋) |
23 | 4, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝑋) |
24 | | fvelrnb 6153 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑋 → (+∞ ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (+∞ ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
26 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (+∞ ∈ ran
𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
27 | 6, 26 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞) |
28 | | snelpwi 4839 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ 𝒫 𝑋) |
29 | | snfi 7923 |
. . . . . . . . . . . . 13
⊢ {𝑦} ∈ Fin |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ Fin) |
31 | 28, 30 | elind 3760 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
32 | 31 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
33 | | simp2 1055 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝑦 ∈ 𝑋) |
34 | 4 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝐹:𝑋⟶(0[,]+∞)) |
35 | 33 | snssd 4281 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → {𝑦} ⊆ 𝑋) |
36 | 34, 35 | fssresd 5984 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹 ↾ {𝑦}):{𝑦}⟶(0[,]+∞)) |
37 | 33, 36 | sge0sn 39272 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) →
(Σ^‘(𝐹 ↾ {𝑦})) = ((𝐹 ↾ {𝑦})‘𝑦)) |
38 | | vsnid 4156 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ {𝑦} |
39 | | fvres 6117 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {𝑦} → ((𝐹 ↾ {𝑦})‘𝑦) = (𝐹‘𝑦)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝐹 ↾ {𝑦})‘𝑦) = (𝐹‘𝑦) |
41 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ((𝐹 ↾ {𝑦})‘𝑦) = (𝐹‘𝑦)) |
42 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) = +∞) |
43 | 37, 41, 42 | 3eqtrrd 2649 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ =
(Σ^‘(𝐹 ↾ {𝑦}))) |
44 | | reseq2 5312 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {𝑦} → (𝐹 ↾ 𝑥) = (𝐹 ↾ {𝑦})) |
45 | 44 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑥 = {𝑦} →
(Σ^‘(𝐹 ↾ 𝑥)) =
(Σ^‘(𝐹 ↾ {𝑦}))) |
46 | 45 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑦} → (+∞ =
(Σ^‘(𝐹 ↾ 𝑥)) ↔ +∞ =
(Σ^‘(𝐹 ↾ {𝑦})))) |
47 | 46 | rspcev 3282 |
. . . . . . . . . 10
⊢ (({𝑦} ∈ (𝒫 𝑋 ∩ Fin) ∧ +∞ =
(Σ^‘(𝐹 ↾ {𝑦}))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ =
(Σ^‘(𝐹 ↾ 𝑥))) |
48 | 32, 43, 47 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ =
(Σ^‘(𝐹 ↾ 𝑥))) |
49 | | pnfex 9972 |
. . . . . . . . . 10
⊢ +∞
∈ V |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈
V) |
51 | 19, 48, 50 | elrnmptd 38361 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))) |
52 | 51 | 3exp 1256 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝑋 → ((𝐹‘𝑦) = +∞ → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))))) |
53 | 52 | rexlimdv 3012 |
. . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞ → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))))) |
54 | 53 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞ → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))))) |
55 | 27, 54 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))) |
56 | | supxrpnf 12020 |
. . . 4
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆ ℝ* ∧
+∞ ∈ ran (𝑥
∈ (𝒫 𝑋 ∩
Fin) ↦ (Σ^‘(𝐹 ↾ 𝑥)))) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞) |
57 | 21, 55, 56 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞) |
58 | 1, 7, 57 | 3eqtr4d 2654 |
. 2
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, <
)) |
59 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝑋 ∈ 𝑉) |
60 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,]+∞)) |
61 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ¬ +∞
∈ ran 𝐹) |
62 | 60, 61 | fge0iccico 39263 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,)+∞)) |
63 | 59, 62 | sge0reval 39265 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
64 | | elinel2 3762 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin) |
65 | 64 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
66 | 15 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
67 | | nelrnres 38369 |
. . . . . . . . . 10
⊢ (¬
+∞ ∈ ran 𝐹
→ ¬ +∞ ∈ ran (𝐹 ↾ 𝑥)) |
68 | 67 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ¬ +∞ ∈
ran (𝐹 ↾ 𝑥)) |
69 | 66, 68 | fge0iccico 39263 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,)+∞)) |
70 | 65, 69 | sge0fsum 39280 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) = Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑥)‘𝑦)) |
71 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
72 | | fvres 6117 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑦) = (𝐹‘𝑦)) |
73 | 71, 72 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑦) = (𝐹‘𝑦)) |
74 | 73 | sumeq2dv 14281 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑥)‘𝑦) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
75 | 74 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑥)‘𝑦) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
76 | 70, 75 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
77 | 76 | mpteq2dva 4672 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
78 | 77 | rneqd 5274 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) = ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
79 | 78 | supeq1d 8235 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
80 | 63, 79 | eqtr4d 2647 |
. 2
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, <
)) |
81 | 58, 80 | pm2.61dan 828 |
1
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, <
)) |