| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . . . 5
⊢ (𝐹 = ∅ →
(Σ^‘𝐹) =
(Σ^‘∅)) | 
| 2 |  | sge00 46396 | . . . . . 6
⊢
(Σ^‘∅) = 0 | 
| 3 | 2 | a1i 11 | . . . . 5
⊢ (𝐹 = ∅ →
(Σ^‘∅) = 0) | 
| 4 | 1, 3 | eqtrd 2776 | . . . 4
⊢ (𝐹 = ∅ →
(Σ^‘𝐹) = 0) | 
| 5 |  | 0e0iccpnf 13500 | . . . . 5
⊢ 0 ∈
(0[,]+∞) | 
| 6 | 5 | a1i 11 | . . . 4
⊢ (𝐹 = ∅ → 0 ∈
(0[,]+∞)) | 
| 7 | 4, 6 | eqeltrd 2840 | . . 3
⊢ (𝐹 = ∅ →
(Σ^‘𝐹) ∈ (0[,]+∞)) | 
| 8 | 7 | adantl 481 | . 2
⊢ ((𝜑 ∧ 𝐹 = ∅) →
(Σ^‘𝐹) ∈ (0[,]+∞)) | 
| 9 |  | sge0cl.x | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 10 | 9 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝑋 ∈ 𝑉) | 
| 11 |  | sge0cl.f | . . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | 
| 12 | 11 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,]+∞)) | 
| 13 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐹) | 
| 14 | 10, 12, 13 | sge0pnfval 46393 | . . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = +∞) | 
| 15 |  | pnfel0pnf 45546 | . . . . . 6
⊢ +∞
∈ (0[,]+∞) | 
| 16 | 15 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈
(0[,]+∞)) | 
| 17 | 14, 16 | eqeltrd 2840 | . . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) ∈ (0[,]+∞)) | 
| 18 | 17 | adantlr 715 | . . 3
⊢ (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) ∈ (0[,]+∞)) | 
| 19 |  | simpll 766 | . . . 4
⊢ (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran
𝐹) → 𝜑) | 
| 20 |  | neqne 2947 | . . . . 5
⊢ (¬
𝐹 = ∅ → 𝐹 ≠ ∅) | 
| 21 | 20 | ad2antlr 727 | . . . 4
⊢ (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹 ≠ ∅) | 
| 22 |  | simpr 484 | . . . 4
⊢ (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran
𝐹) → ¬ +∞
∈ ran 𝐹) | 
| 23 |  | 0xr 11309 | . . . . . 6
⊢ 0 ∈
ℝ* | 
| 24 | 23 | a1i 11 | . . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → 0 ∈
ℝ*) | 
| 25 |  | pnfxr 11316 | . . . . . 6
⊢ +∞
∈ ℝ* | 
| 26 | 25 | a1i 11 | . . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → +∞
∈ ℝ*) | 
| 27 | 9 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝑋 ∈ 𝑉) | 
| 28 | 11 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,]+∞)) | 
| 29 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ¬ +∞
∈ ran 𝐹) | 
| 30 | 28, 29 | fge0iccico 46390 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,)+∞)) | 
| 31 | 27, 30 | sge0reval 46392 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) | 
| 32 |  | elinel2 4201 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin) | 
| 33 | 32 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) | 
| 34 | 11 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝐹:𝑋⟶(0[,]+∞)) | 
| 35 |  | elinel1 4200 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ 𝒫 𝑋) | 
| 36 |  | elpwi 4606 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) | 
| 37 | 35, 36 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋) | 
| 38 | 37 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋) | 
| 39 | 38 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑥 ⊆ 𝑋) | 
| 40 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) | 
| 41 | 39, 40 | sseldd 3983 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) | 
| 42 | 34, 41 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,]+∞)) | 
| 43 | 42 | adantllr 719 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,]+∞)) | 
| 44 |  | nne 2943 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝐹‘𝑦) ≠ +∞ ↔ (𝐹‘𝑦) = +∞) | 
| 45 | 44 | biimpi 216 | . . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐹‘𝑦) ≠ +∞ → (𝐹‘𝑦) = +∞) | 
| 46 | 45 | eqcomd 2742 | . . . . . . . . . . . . . . . 16
⊢ (¬
(𝐹‘𝑦) ≠ +∞ → +∞ = (𝐹‘𝑦)) | 
| 47 | 46 | adantl 481 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ ¬ (𝐹‘𝑦) ≠ +∞) → +∞ = (𝐹‘𝑦)) | 
| 48 | 11 | ffund 6739 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Fun 𝐹) | 
| 49 | 48 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → Fun 𝐹) | 
| 50 | 41 | 3impa 1109 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) | 
| 51 | 11 | fdmd 6745 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → dom 𝐹 = 𝑋) | 
| 52 | 51 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 = dom 𝐹) | 
| 53 | 52 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑋 = dom 𝐹) | 
| 54 | 50, 53 | eleqtrd 2842 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ dom 𝐹) | 
| 55 |  | fvelrn 7095 | . . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ ran 𝐹) | 
| 56 | 49, 54, 55 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ran 𝐹) | 
| 57 | 56 | ad5ant134 1368 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ ¬ (𝐹‘𝑦) ≠ +∞) → (𝐹‘𝑦) ∈ ran 𝐹) | 
| 58 | 47, 57 | eqeltrd 2840 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ ¬ (𝐹‘𝑦) ≠ +∞) → +∞ ∈ ran
𝐹) | 
| 59 | 29 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ ¬ (𝐹‘𝑦) ≠ +∞) → ¬ +∞ ∈
ran 𝐹) | 
| 60 | 58, 59 | condan 817 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ≠ +∞) | 
| 61 |  | ge0xrre 45549 | . . . . . . . . . . . . 13
⊢ (((𝐹‘𝑦) ∈ (0[,]+∞) ∧ (𝐹‘𝑦) ≠ +∞) → (𝐹‘𝑦) ∈ ℝ) | 
| 62 | 43, 60, 61 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℝ) | 
| 63 | 33, 62 | fsumrecl 15771 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ℝ) | 
| 64 | 63 | ralrimiva 3145 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ℝ) | 
| 65 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) | 
| 66 | 65 | rnmptss 7142 | . . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ℝ → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ) | 
| 67 | 64, 66 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ) | 
| 68 |  | ressxr 11306 | . . . . . . . . . 10
⊢ ℝ
⊆ ℝ* | 
| 69 | 68 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ℝ ⊆
ℝ*) | 
| 70 | 67, 69 | sstrd 3993 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆
ℝ*) | 
| 71 |  | supxrcl 13358 | . . . . . . . 8
⊢ (ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ* → sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) ∈
ℝ*) | 
| 72 | 70, 71 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) ∈
ℝ*) | 
| 73 | 31, 72 | eqeltrd 2840 | . . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) ∈
ℝ*) | 
| 74 | 73 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) →
(Σ^‘𝐹) ∈
ℝ*) | 
| 75 | 52 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → 𝑋 = dom 𝐹) | 
| 76 |  | neneq 2945 | . . . . . . . . . . . 12
⊢ (𝐹 ≠ ∅ → ¬ 𝐹 = ∅) | 
| 77 | 76 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → ¬ 𝐹 = ∅) | 
| 78 |  | frel 6740 | . . . . . . . . . . . . . 14
⊢ (𝐹:𝑋⟶(0[,]+∞) → Rel 𝐹) | 
| 79 | 11, 78 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → Rel 𝐹) | 
| 80 | 79 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → Rel 𝐹) | 
| 81 |  | reldm0 5937 | . . . . . . . . . . . 12
⊢ (Rel
𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) | 
| 82 | 80, 81 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) | 
| 83 | 77, 82 | mtbid 324 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → ¬ dom 𝐹 = ∅) | 
| 84 | 83 | neqned 2946 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → dom 𝐹 ≠ ∅) | 
| 85 | 75, 84 | eqnetrd 3007 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → 𝑋 ≠ ∅) | 
| 86 |  | n0 4352 | . . . . . . . 8
⊢ (𝑋 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝑋) | 
| 87 | 85, 86 | sylib 218 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → ∃𝑧 𝑧 ∈ 𝑋) | 
| 88 | 87 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → ∃𝑧 𝑧 ∈ 𝑋) | 
| 89 | 23 | a1i 11 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → 0 ∈
ℝ*) | 
| 90 | 11 | ffvelcdmda 7103 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ (0[,]+∞)) | 
| 91 | 90 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ (0[,]+∞)) | 
| 92 |  | nne 2943 | . . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐹‘𝑧) ≠ +∞ ↔ (𝐹‘𝑧) = +∞) | 
| 93 | 92 | biimpi 216 | . . . . . . . . . . . . . . . 16
⊢ (¬
(𝐹‘𝑧) ≠ +∞ → (𝐹‘𝑧) = +∞) | 
| 94 | 93 | eqcomd 2742 | . . . . . . . . . . . . . . 15
⊢ (¬
(𝐹‘𝑧) ≠ +∞ → +∞ = (𝐹‘𝑧)) | 
| 95 | 94 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) ∧ ¬ (𝐹‘𝑧) ≠ +∞) → +∞ = (𝐹‘𝑧)) | 
| 96 | 11 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) | 
| 97 | 96 | ffund 6739 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → Fun 𝐹) | 
| 98 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) | 
| 99 | 52 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑋 = dom 𝐹) | 
| 100 | 98, 99 | eleqtrd 2842 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ dom 𝐹) | 
| 101 |  | fvelrn 7095 | . . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐹 ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ran 𝐹) | 
| 102 | 97, 100, 101 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ran 𝐹) | 
| 103 | 102 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ran 𝐹) | 
| 104 | 103 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) ∧ ¬ (𝐹‘𝑧) ≠ +∞) → (𝐹‘𝑧) ∈ ran 𝐹) | 
| 105 | 95, 104 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) ∧ ¬ (𝐹‘𝑧) ≠ +∞) → +∞ ∈ ran
𝐹) | 
| 106 | 29 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) ∧ ¬ (𝐹‘𝑧) ≠ +∞) → ¬ +∞ ∈
ran 𝐹) | 
| 107 | 105, 106 | condan 817 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ≠ +∞) | 
| 108 |  | ge0xrre 45549 | . . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ (0[,]+∞) ∧ (𝐹‘𝑧) ≠ +∞) → (𝐹‘𝑧) ∈ ℝ) | 
| 109 | 91, 107, 108 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℝ) | 
| 110 | 109 | rexrd 11312 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈
ℝ*) | 
| 111 | 73 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) →
(Σ^‘𝐹) ∈
ℝ*) | 
| 112 | 23 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 0 ∈
ℝ*) | 
| 113 | 25 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → +∞ ∈
ℝ*) | 
| 114 |  | iccgelb 13444 | . . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑧) ∈ (0[,]+∞)) → 0 ≤ (𝐹‘𝑧)) | 
| 115 | 112, 113,
90, 114 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 0 ≤ (𝐹‘𝑧)) | 
| 116 | 115 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → 0 ≤ (𝐹‘𝑧)) | 
| 117 | 70 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆
ℝ*) | 
| 118 |  | snelpwi 5447 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑋 → {𝑧} ∈ 𝒫 𝑋) | 
| 119 |  | snfi 9084 | . . . . . . . . . . . . . . . . 17
⊢ {𝑧} ∈ Fin | 
| 120 | 119 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑋 → {𝑧} ∈ Fin) | 
| 121 | 118, 120 | elind 4199 | . . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑋 → {𝑧} ∈ (𝒫 𝑋 ∩ Fin)) | 
| 122 | 121 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → {𝑧} ∈ (𝒫 𝑋 ∩ Fin)) | 
| 123 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) | 
| 124 | 109 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ) | 
| 125 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) | 
| 126 | 125 | sumsn 15783 | . . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ ℂ) → Σ𝑦 ∈ {𝑧} (𝐹‘𝑦) = (𝐹‘𝑧)) | 
| 127 | 123, 124,
126 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → Σ𝑦 ∈ {𝑧} (𝐹‘𝑦) = (𝐹‘𝑧)) | 
| 128 | 127 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = Σ𝑦 ∈ {𝑧} (𝐹‘𝑦)) | 
| 129 |  | sumeq1 15726 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = {𝑧} → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = Σ𝑦 ∈ {𝑧} (𝐹‘𝑦)) | 
| 130 | 129 | rspceeqv 3644 | . . . . . . . . . . . . . 14
⊢ (({𝑧} ∈ (𝒫 𝑋 ∩ Fin) ∧ (𝐹‘𝑧) = Σ𝑦 ∈ {𝑧} (𝐹‘𝑦)) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑧) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) | 
| 131 | 122, 128,
130 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑧) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) | 
| 132 | 65 | elrnmpt 5968 | . . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑧) ∈ (0[,]+∞) → ((𝐹‘𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑧) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) | 
| 133 | 91, 132 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑧) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) | 
| 134 | 131, 133 | mpbird 257 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) | 
| 135 |  | supxrub 13367 | . . . . . . . . . . . 12
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ* ∧ (𝐹‘𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → (𝐹‘𝑧) ≤ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) | 
| 136 | 117, 134,
135 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ≤ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) | 
| 137 | 31 | eqcomd 2742 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) =
(Σ^‘𝐹)) | 
| 138 | 137 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) =
(Σ^‘𝐹)) | 
| 139 | 136, 138 | breqtrd 5168 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ≤
(Σ^‘𝐹)) | 
| 140 | 89, 110, 111, 116, 139 | xrletrd 13205 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → 0 ≤
(Σ^‘𝐹)) | 
| 141 | 140 | ex 412 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → (𝑧 ∈ 𝑋 → 0 ≤
(Σ^‘𝐹))) | 
| 142 | 141 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → (𝑧 ∈ 𝑋 → 0 ≤
(Σ^‘𝐹))) | 
| 143 | 142 | exlimdv 1932 | . . . . . 6
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → (∃𝑧 𝑧 ∈ 𝑋 → 0 ≤
(Σ^‘𝐹))) | 
| 144 | 88, 143 | mpd 15 | . . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → 0 ≤
(Σ^‘𝐹)) | 
| 145 |  | pnfge 13173 | . . . . . . 7
⊢
((Σ^‘𝐹) ∈ ℝ* →
(Σ^‘𝐹) ≤ +∞) | 
| 146 | 73, 145 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) ≤ +∞) | 
| 147 | 146 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) →
(Σ^‘𝐹) ≤ +∞) | 
| 148 | 24, 26, 74, 144, 147 | eliccxrd 45545 | . . . 4
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) →
(Σ^‘𝐹) ∈ (0[,]+∞)) | 
| 149 | 19, 21, 22, 148 | syl21anc 837 | . . 3
⊢ (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) ∈ (0[,]+∞)) | 
| 150 | 18, 149 | pm2.61dan 812 | . 2
⊢ ((𝜑 ∧ ¬ 𝐹 = ∅) →
(Σ^‘𝐹) ∈ (0[,]+∞)) | 
| 151 | 8, 150 | pm2.61dan 812 | 1
⊢ (𝜑 →
(Σ^‘𝐹) ∈ (0[,]+∞)) |