| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sge0fsum.x | . . 3
⊢ (𝜑 → 𝑋 ∈ Fin) | 
| 2 |  | sge0fsum.f | . . . 4
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) | 
| 3 | 2 | fge0icoicc 46380 | . . 3
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | 
| 4 | 1, 3 | sge0xrcl 46400 | . 2
⊢ (𝜑 →
(Σ^‘𝐹) ∈
ℝ*) | 
| 5 |  | rge0ssre 13496 | . . . . 5
⊢
(0[,)+∞) ⊆ ℝ | 
| 6 | 2 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (0[,)+∞)) | 
| 7 | 5, 6 | sselid 3981 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℝ) | 
| 8 | 1, 7 | fsumrecl 15770 | . . 3
⊢ (𝜑 → Σ𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ ℝ) | 
| 9 | 8 | rexrd 11311 | . 2
⊢ (𝜑 → Σ𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈
ℝ*) | 
| 10 | 1, 2 | sge0reval 46387 | . . 3
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)), ℝ*, <
)) | 
| 11 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))) → 𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))) | 
| 12 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑤 ∈ V | 
| 13 | 12 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))) → 𝑤 ∈ V) | 
| 14 |  | eqid 2737 | . . . . . . . . 9
⊢ (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) = (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) | 
| 15 | 14 | elrnmpt 5969 | . . . . . . . 8
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) ↔ ∃𝑦 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))) | 
| 16 | 13, 15 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))) → (𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) ↔ ∃𝑦 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))) | 
| 17 | 11, 16 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))) → ∃𝑦 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) | 
| 18 |  | simp3 1139 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑤 = Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) → 𝑤 = Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) | 
| 19 | 1 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑋 ∈ Fin) | 
| 20 | 2 | fge0npnf 46382 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ +∞ ∈ ran
𝐹) | 
| 21 | 3, 20 | fge0iccre 46389 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶ℝ) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑋) → 𝐹:𝑋⟶ℝ) | 
| 24 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 25 | 23, 24 | ffvelcdmd 7105 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℝ) | 
| 26 |  | 0xr 11308 | . . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ* | 
| 27 | 26 | a1i 11 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑋) → 0 ∈
ℝ*) | 
| 28 |  | pnfxr 11315 | . . . . . . . . . . . . . 14
⊢ +∞
∈ ℝ* | 
| 29 | 28 | a1i 11 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑋) → +∞ ∈
ℝ*) | 
| 30 | 3 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞)) | 
| 31 | 30 | ffvelcdmda 7104 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (0[,]+∞)) | 
| 32 |  | iccgelb 13443 | . . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑥) ∈ (0[,]+∞)) → 0 ≤ (𝐹‘𝑥)) | 
| 33 | 27, 29, 31, 32 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝐹‘𝑥)) | 
| 34 |  | elinel1 4201 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝑋 ∩ Fin) → 𝑦 ∈ 𝒫 𝑋) | 
| 35 |  | elpwi 4607 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋) | 
| 36 | 34, 35 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 𝑋 ∩ Fin) → 𝑦 ⊆ 𝑋) | 
| 37 | 36 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑦 ⊆ 𝑋) | 
| 38 | 19, 25, 33, 37 | fsumless 15832 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (𝐹‘𝑥) ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥)) | 
| 39 | 38 | 3adant3 1133 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑤 = Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) → Σ𝑥 ∈ 𝑦 (𝐹‘𝑥) ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥)) | 
| 40 | 18, 39 | eqbrtrd 5165 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑤 = Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) → 𝑤 ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥)) | 
| 41 | 40 | 3exp 1120 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝒫 𝑋 ∩ Fin) → (𝑤 = Σ𝑥 ∈ 𝑦 (𝐹‘𝑥) → 𝑤 ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥)))) | 
| 42 | 41 | rexlimdv 3153 | . . . . . . 7
⊢ (𝜑 → (∃𝑦 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑥 ∈ 𝑦 (𝐹‘𝑥) → 𝑤 ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥))) | 
| 43 | 42 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))) → (∃𝑦 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑥 ∈ 𝑦 (𝐹‘𝑥) → 𝑤 ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥))) | 
| 44 | 17, 43 | mpd 15 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))) → 𝑤 ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥)) | 
| 45 | 44 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))𝑤 ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥)) | 
| 46 |  | elinel2 4202 | . . . . . . . . . 10
⊢ (𝑦 ∈ (𝒫 𝑋 ∩ Fin) → 𝑦 ∈ Fin) | 
| 47 | 46 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑦 ∈ Fin) | 
| 48 | 22 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝐹:𝑋⟶ℝ) | 
| 49 | 37 | sselda 3983 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝑋) | 
| 50 | 48, 49 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (𝐹‘𝑥) ∈ ℝ) | 
| 51 | 47, 50 | fsumrecl 15770 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (𝐹‘𝑥) ∈ ℝ) | 
| 52 | 51 | rexrd 11311 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (𝐹‘𝑥) ∈
ℝ*) | 
| 53 | 52 | ralrimiva 3146 | . . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ (𝒫 𝑋 ∩ Fin)Σ𝑥 ∈ 𝑦 (𝐹‘𝑥) ∈
ℝ*) | 
| 54 | 14 | rnmptss 7143 | . . . . . 6
⊢
(∀𝑦 ∈
(𝒫 𝑋 ∩
Fin)Σ𝑥 ∈ 𝑦 (𝐹‘𝑥) ∈ ℝ* → ran
(𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) ⊆
ℝ*) | 
| 55 | 53, 54 | syl 17 | . . . . 5
⊢ (𝜑 → ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) ⊆
ℝ*) | 
| 56 |  | supxrleub 13368 | . . . . 5
⊢ ((ran
(𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)) ⊆ ℝ* ∧
Σ𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ ℝ*) → (sup(ran
(𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)), ℝ*, < ) ≤
Σ𝑥 ∈ 𝑋 (𝐹‘𝑥) ↔ ∀𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))𝑤 ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥))) | 
| 57 | 55, 9, 56 | syl2anc 584 | . . . 4
⊢ (𝜑 → (sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)), ℝ*, < ) ≤
Σ𝑥 ∈ 𝑋 (𝐹‘𝑥) ↔ ∀𝑤 ∈ ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥))𝑤 ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥))) | 
| 58 | 45, 57 | mpbird 257 | . . 3
⊢ (𝜑 → sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑥 ∈ 𝑦 (𝐹‘𝑥)), ℝ*, < ) ≤
Σ𝑥 ∈ 𝑋 (𝐹‘𝑥)) | 
| 59 | 10, 58 | eqbrtrd 5165 | . 2
⊢ (𝜑 →
(Σ^‘𝐹) ≤ Σ𝑥 ∈ 𝑋 (𝐹‘𝑥)) | 
| 60 |  | ssid 4006 | . . . 4
⊢ 𝑋 ⊆ 𝑋 | 
| 61 | 60 | a1i 11 | . . 3
⊢ (𝜑 → 𝑋 ⊆ 𝑋) | 
| 62 | 1, 2, 61, 1 | fsumlesge0 46392 | . 2
⊢ (𝜑 → Σ𝑥 ∈ 𝑋 (𝐹‘𝑥) ≤
(Σ^‘𝐹)) | 
| 63 | 4, 9, 59, 62 | xrletrid 13197 | 1
⊢ (𝜑 →
(Σ^‘𝐹) = Σ𝑥 ∈ 𝑋 (𝐹‘𝑥)) |