| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sge0supre.x | . . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 2 |  | sge0supre.f | . . . 4
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | 
| 3 | 1 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝑋 ∈ 𝑉) | 
| 4 | 2 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,]+∞)) | 
| 5 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐹) | 
| 6 | 3, 4, 5 | sge0pnfval 46388 | . . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = +∞) | 
| 7 |  | sge0supre.re | . . . . . . 7
⊢ (𝜑 →
(Σ^‘𝐹) ∈ ℝ) | 
| 8 | 1, 2 | sge0repnf 46401 | . . . . . . 7
⊢ (𝜑 →
((Σ^‘𝐹) ∈ ℝ ↔ ¬
(Σ^‘𝐹) = +∞)) | 
| 9 | 7, 8 | mpbid 232 | . . . . . 6
⊢ (𝜑 → ¬
(Σ^‘𝐹) = +∞) | 
| 10 | 9 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ¬
(Σ^‘𝐹) = +∞) | 
| 11 | 6, 10 | pm2.65da 817 | . . . 4
⊢ (𝜑 → ¬ +∞ ∈ ran
𝐹) | 
| 12 | 2, 11 | fge0iccico 46385 | . . 3
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) | 
| 13 | 1, 12 | sge0reval 46387 | . 2
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) | 
| 14 | 12 | sge0rnre 46379 | . . 3
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ) | 
| 15 |  | sge0rnn0 46383 | . . . 4
⊢ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅ | 
| 16 | 15 | a1i 11 | . . 3
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅) | 
| 17 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) | 
| 18 |  | eqid 2737 | . . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) | 
| 19 | 18 | elrnmpt 5969 | . . . . . . . 8
⊢ (𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) | 
| 20 | 19 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → (𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) | 
| 21 | 17, 20 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) | 
| 22 |  | simp3 1139 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) | 
| 23 |  | ressxr 11305 | . . . . . . . . . . . . . . . 16
⊢ ℝ
⊆ ℝ* | 
| 24 | 23 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ℝ ⊆
ℝ*) | 
| 25 | 14, 24 | sstrd 3994 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆
ℝ*) | 
| 26 | 25 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆
ℝ*) | 
| 27 |  | id 22 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) | 
| 28 |  | sumex 15724 | . . . . . . . . . . . . . . . 16
⊢
Σ𝑦 ∈
𝑥 (𝐹‘𝑦) ∈ V | 
| 29 | 28 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ V) | 
| 30 | 18 | elrnmpt1 5971 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ V) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) | 
| 31 | 27, 29, 30 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) | 
| 32 | 31 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) | 
| 33 |  | supxrub 13366 | . . . . . . . . . . . . 13
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ* ∧
Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) | 
| 34 | 26, 32, 33 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) | 
| 35 | 13 | eqcomd 2743 | . . . . . . . . . . . . 13
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) =
(Σ^‘𝐹)) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) =
(Σ^‘𝐹)) | 
| 37 | 34, 36 | breqtrd 5169 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤
(Σ^‘𝐹)) | 
| 38 | 37 | 3adant3 1133 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤
(Σ^‘𝐹)) | 
| 39 | 22, 38 | eqbrtrd 5165 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑤 ≤
(Σ^‘𝐹)) | 
| 40 | 39 | 3exp 1120 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → (𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑤 ≤
(Σ^‘𝐹)))) | 
| 41 | 40 | rexlimdv 3153 | . . . . . . 7
⊢ (𝜑 → (∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑤 ≤
(Σ^‘𝐹))) | 
| 42 | 41 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → (∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑤 ≤
(Σ^‘𝐹))) | 
| 43 | 21, 42 | mpd 15 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → 𝑤 ≤
(Σ^‘𝐹)) | 
| 44 | 43 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤
(Σ^‘𝐹)) | 
| 45 |  | brralrspcev 5203 | . . . 4
⊢
(((Σ^‘𝐹) ∈ ℝ ∧ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤
(Σ^‘𝐹)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤ 𝑧) | 
| 46 | 7, 44, 45 | syl2anc 584 | . . 3
⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤ 𝑧) | 
| 47 |  | supxrre 13369 | . . 3
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤ 𝑧) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )) | 
| 48 | 14, 16, 46, 47 | syl3anc 1373 | . 2
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )) | 
| 49 | 13, 48 | eqtrd 2777 | 1
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )) |