| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. . 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 484 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐹) |
| 7 | 3, 5, 6 | sge0pnfval 46388 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = +∞) |
| 8 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 9 | 8 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ V) |
| 10 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞)) |
| 11 | | elinel1 4201 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ 𝒫 𝑋) |
| 12 | | elpwi 4607 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋) |
| 14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋) |
| 15 | 10, 14 | fssresd 6775 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
| 16 | 9, 15 | sge0xrcl 46400 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) |
| 17 | 16 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ +∞ ∈ ran 𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) |
| 18 | 17 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ∀𝑥 ∈ (𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ∈
ℝ*) |
| 19 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) |
| 20 | 19 | rnmptss 7143 |
. . . . 5
⊢
(∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(Σ^‘(𝐹 ↾ 𝑥)) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆
ℝ*) |
| 21 | 18, 20 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆
ℝ*) |
| 22 | 4 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝑋) |
| 23 | | fvelrnb 6969 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑋 → (+∞ ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
| 24 | 22, 23 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (+∞ ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
| 25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (+∞ ∈ ran
𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
| 26 | 6, 25 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞) |
| 27 | | snelpwi 5448 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ 𝒫 𝑋) |
| 28 | | snfi 9083 |
. . . . . . . . . . . . 13
⊢ {𝑦} ∈ Fin |
| 29 | 28 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ Fin) |
| 30 | 27, 29 | elind 4200 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
| 31 | 30 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
| 32 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝑦 ∈ 𝑋) |
| 33 | 4 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝐹:𝑋⟶(0[,]+∞)) |
| 34 | 32 | snssd 4809 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → {𝑦} ⊆ 𝑋) |
| 35 | 33, 34 | fssresd 6775 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹 ↾ {𝑦}):{𝑦}⟶(0[,]+∞)) |
| 36 | 32, 35 | sge0sn 46394 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) →
(Σ^‘(𝐹 ↾ {𝑦})) = ((𝐹 ↾ {𝑦})‘𝑦)) |
| 37 | | vsnid 4663 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ {𝑦} |
| 38 | | fvres 6925 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {𝑦} → ((𝐹 ↾ {𝑦})‘𝑦) = (𝐹‘𝑦)) |
| 39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝐹 ↾ {𝑦})‘𝑦) = (𝐹‘𝑦) |
| 40 | 39 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ((𝐹 ↾ {𝑦})‘𝑦) = (𝐹‘𝑦)) |
| 41 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) = +∞) |
| 42 | 36, 40, 41 | 3eqtrrd 2782 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ =
(Σ^‘(𝐹 ↾ {𝑦}))) |
| 43 | | reseq2 5992 |
. . . . . . . . . . . 12
⊢ (𝑥 = {𝑦} → (𝐹 ↾ 𝑥) = (𝐹 ↾ {𝑦})) |
| 44 | 43 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑦} →
(Σ^‘(𝐹 ↾ 𝑥)) =
(Σ^‘(𝐹 ↾ {𝑦}))) |
| 45 | 44 | rspceeqv 3645 |
. . . . . . . . . 10
⊢ (({𝑦} ∈ (𝒫 𝑋 ∩ Fin) ∧ +∞ =
(Σ^‘(𝐹 ↾ {𝑦}))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ =
(Σ^‘(𝐹 ↾ 𝑥))) |
| 46 | 31, 42, 45 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ =
(Σ^‘(𝐹 ↾ 𝑥))) |
| 47 | | pnfex 11314 |
. . . . . . . . . 10
⊢ +∞
∈ V |
| 48 | 47 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈
V) |
| 49 | 19, 46, 48 | elrnmptd 5974 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))) |
| 50 | 49 | 3exp 1120 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝑋 → ((𝐹‘𝑦) = +∞ → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))))) |
| 51 | 50 | rexlimdv 3153 |
. . . . . 6
⊢ (𝜑 → (∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞ → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))))) |
| 52 | 51 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞ → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))))) |
| 53 | 26, 52 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥)))) |
| 54 | | supxrpnf 13360 |
. . . 4
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) ⊆ ℝ* ∧
+∞ ∈ ran (𝑥
∈ (𝒫 𝑋 ∩
Fin) ↦ (Σ^‘(𝐹 ↾ 𝑥)))) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞) |
| 55 | 21, 53, 54 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞) |
| 56 | 1, 7, 55 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, <
)) |
| 57 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝑋 ∈ 𝑉) |
| 58 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,]+∞)) |
| 59 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ¬ +∞
∈ ran 𝐹) |
| 60 | 58, 59 | fge0iccico 46385 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,)+∞)) |
| 61 | 57, 60 | sge0reval 46387 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
| 62 | | elinel2 4202 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin) |
| 63 | 62 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
| 64 | 15 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
| 65 | | nelrnres 45192 |
. . . . . . . . . 10
⊢ (¬
+∞ ∈ ran 𝐹
→ ¬ +∞ ∈ ran (𝐹 ↾ 𝑥)) |
| 66 | 65 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ¬ +∞ ∈
ran (𝐹 ↾ 𝑥)) |
| 67 | 64, 66 | fge0iccico 46385 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,)+∞)) |
| 68 | 63, 67 | sge0fsum 46402 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) = Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑥)‘𝑦)) |
| 69 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
| 70 | | fvres 6925 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑦) = (𝐹‘𝑦)) |
| 71 | 69, 70 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝑥)‘𝑦) = (𝐹‘𝑦)) |
| 72 | 71 | sumeq2dv 15738 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑥)‘𝑦) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
| 73 | 72 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑥)‘𝑦) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
| 74 | 68, 73 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝑥)) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
| 75 | 74 | mpteq2dva 5242 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
| 76 | 75 | rneqd 5949 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))) = ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
| 77 | 76 | supeq1d 9486 |
. . 3
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
| 78 | 61, 77 | eqtr4d 2780 |
. 2
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, <
)) |
| 79 | 56, 78 | pm2.61dan 813 |
1
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦
(Σ^‘(𝐹 ↾ 𝑥))), ℝ*, <
)) |