| Step | Hyp | Ref
| Expression |
| 1 | | sge0less.1 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 2 | | inex1g 5319 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∩ 𝑌) ∈ V) |
| 3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∩ 𝑌) ∈ V) |
| 4 | | sge0less.2 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
| 5 | | fresin 6777 |
. . . . . . 7
⊢ (𝐹:𝑋⟶(0[,]+∞) → (𝐹 ↾ 𝑌):(𝑋 ∩ 𝑌)⟶(0[,]+∞)) |
| 6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ 𝑌):(𝑋 ∩ 𝑌)⟶(0[,]+∞)) |
| 7 | 3, 6 | sge0xrcl 46400 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝐹 ↾ 𝑌)) ∈
ℝ*) |
| 8 | | pnfge 13172 |
. . . . 5
⊢
((Σ^‘(𝐹 ↾ 𝑌)) ∈ ℝ* →
(Σ^‘(𝐹 ↾ 𝑌)) ≤ +∞) |
| 9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝐹 ↾ 𝑌)) ≤ +∞) |
| 10 | 9 | adantr 480 |
. . 3
⊢ ((𝜑 ∧
(Σ^‘𝐹) = +∞) →
(Σ^‘(𝐹 ↾ 𝑌)) ≤ +∞) |
| 11 | | id 22 |
. . . . 5
⊢
((Σ^‘𝐹) = +∞ →
(Σ^‘𝐹) = +∞) |
| 12 | 11 | eqcomd 2743 |
. . . 4
⊢
((Σ^‘𝐹) = +∞ → +∞ =
(Σ^‘𝐹)) |
| 13 | 12 | adantl 481 |
. . 3
⊢ ((𝜑 ∧
(Σ^‘𝐹) = +∞) → +∞ =
(Σ^‘𝐹)) |
| 14 | 10, 13 | breqtrd 5169 |
. 2
⊢ ((𝜑 ∧
(Σ^‘𝐹) = +∞) →
(Σ^‘(𝐹 ↾ 𝑌)) ≤
(Σ^‘𝐹)) |
| 15 | | simpl 482 |
. . 3
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) = +∞) → 𝜑) |
| 16 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) = +∞) → ¬
(Σ^‘𝐹) = +∞) |
| 17 | 15, 1 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) = +∞) → 𝑋 ∈ 𝑉) |
| 18 | 15, 4 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) = +∞) → 𝐹:𝑋⟶(0[,]+∞)) |
| 19 | 17, 18 | sge0repnf 46401 |
. . . 4
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) = +∞) →
((Σ^‘𝐹) ∈ ℝ ↔ ¬
(Σ^‘𝐹) = +∞)) |
| 20 | 16, 19 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) = +∞) →
(Σ^‘𝐹) ∈ ℝ) |
| 21 | | elinel1 4201 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) → 𝑥 ∈ 𝒫 (𝑋 ∩ 𝑌)) |
| 22 | | elpwi 4607 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝒫 (𝑋 ∩ 𝑌) → 𝑥 ⊆ (𝑋 ∩ 𝑌)) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) → 𝑥 ⊆ (𝑋 ∩ 𝑌)) |
| 24 | | inss2 4238 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑌 |
| 25 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) → (𝑋 ∩ 𝑌) ⊆ 𝑌) |
| 26 | 23, 25 | sstrd 3994 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) → 𝑥 ⊆ 𝑌) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑥 ⊆ 𝑌) |
| 28 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
| 29 | 27, 28 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑌) |
| 30 | | fvres 6925 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑌 → ((𝐹 ↾ 𝑌)‘𝑦) = (𝐹‘𝑦)) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ∧ 𝑦 ∈ 𝑥) → ((𝐹 ↾ 𝑌)‘𝑦) = (𝐹‘𝑦)) |
| 32 | 31 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) → ∀𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦) = (𝐹‘𝑦)) |
| 33 | 32 | sumeq2d 15737 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) → Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
| 34 | 33 | mpteq2ia 5245 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)) = (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
| 35 | | inss1 4237 |
. . . . . . . . . . 11
⊢ (𝑋 ∩ 𝑌) ⊆ 𝑋 |
| 36 | 35 | sspwi 4612 |
. . . . . . . . . 10
⊢ 𝒫
(𝑋 ∩ 𝑌) ⊆ 𝒫 𝑋 |
| 37 | | ssrin 4242 |
. . . . . . . . . 10
⊢
(𝒫 (𝑋 ∩
𝑌) ⊆ 𝒫 𝑋 → (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ⊆ (𝒫 𝑋 ∩ Fin)) |
| 38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
⊢
(𝒫 (𝑋 ∩
𝑌) ∩ Fin) ⊆
(𝒫 𝑋 ∩
Fin) |
| 39 | | mptss 6060 |
. . . . . . . . 9
⊢
((𝒫 (𝑋 ∩
𝑌) ∩ Fin) ⊆
(𝒫 𝑋 ∩ Fin)
→ (𝑥 ∈ (𝒫
(𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
| 40 | 38, 39 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
| 41 | 34, 40 | eqsstri 4030 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)) ⊆ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
| 42 | | rnss 5950 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)) ⊆ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ran (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)) ⊆ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
| 43 | 41, 42 | ax-mp 5 |
. . . . . 6
⊢ ran
(𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)) ⊆ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
| 44 | 43 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → ran (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)) ⊆ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
| 45 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → 𝐹:𝑋⟶(0[,]+∞)) |
| 46 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → 𝑋 ∈ 𝑉) |
| 47 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘𝐹) ∈ ℝ) |
| 48 | 46, 45, 47 | sge0rern 46403 |
. . . . . . . 8
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → ¬ +∞
∈ ran 𝐹) |
| 49 | 45, 48 | fge0iccico 46385 |
. . . . . . 7
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → 𝐹:𝑋⟶(0[,)+∞)) |
| 50 | 49 | sge0rnre 46379 |
. . . . . 6
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ) |
| 51 | | ressxr 11305 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
| 52 | 50, 51 | sstrdi 3996 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆
ℝ*) |
| 53 | | supxrss 13374 |
. . . . 5
⊢ ((ran
(𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)) ⊆ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ∧ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ*) →
sup(ran (𝑥 ∈
(𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)), ℝ*, < ) ≤ sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
| 54 | 44, 52, 53 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → sup(ran (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)), ℝ*, < ) ≤ sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
| 55 | 46, 2 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → (𝑋 ∩ 𝑌) ∈ V) |
| 56 | 45, 5 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → (𝐹 ↾ 𝑌):(𝑋 ∩ 𝑌)⟶(0[,]+∞)) |
| 57 | | nelrnres 45192 |
. . . . . . . 8
⊢ (¬
+∞ ∈ ran 𝐹
→ ¬ +∞ ∈ ran (𝐹 ↾ 𝑌)) |
| 58 | 48, 57 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → ¬ +∞
∈ ran (𝐹 ↾ 𝑌)) |
| 59 | 56, 58 | fge0iccico 46385 |
. . . . . 6
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → (𝐹 ↾ 𝑌):(𝑋 ∩ 𝑌)⟶(0[,)+∞)) |
| 60 | 55, 59 | sge0reval 46387 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘(𝐹 ↾ 𝑌)) = sup(ran (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)), ℝ*, <
)) |
| 61 | 46, 49 | sge0reval 46387 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
| 62 | 60, 61 | breq12d 5156 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
((Σ^‘(𝐹 ↾ 𝑌)) ≤
(Σ^‘𝐹) ↔ sup(ran (𝑥 ∈ (𝒫 (𝑋 ∩ 𝑌) ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑌)‘𝑦)), ℝ*, < ) ≤ sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
))) |
| 63 | 54, 62 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘(𝐹 ↾ 𝑌)) ≤
(Σ^‘𝐹)) |
| 64 | 15, 20, 63 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) = +∞) →
(Σ^‘(𝐹 ↾ 𝑌)) ≤
(Σ^‘𝐹)) |
| 65 | 14, 64 | pm2.61dan 813 |
1
⊢ (𝜑 →
(Σ^‘(𝐹 ↾ 𝑌)) ≤
(Σ^‘𝐹)) |