Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝐹 = ∅ →
(Σ^‘𝐹) =
(Σ^‘∅)) |
2 | | sge00 39269 |
. . . . . 6
⊢
(Σ^‘∅) = 0 |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝐹 = ∅ →
(Σ^‘∅) = 0) |
4 | 1, 3 | eqtrd 2644 |
. . . 4
⊢ (𝐹 = ∅ →
(Σ^‘𝐹) = 0) |
5 | | 0e0iccpnf 12154 |
. . . . 5
⊢ 0 ∈
(0[,]+∞) |
6 | 5 | a1i 11 |
. . . 4
⊢ (𝐹 = ∅ → 0 ∈
(0[,]+∞)) |
7 | 4, 6 | eqeltrd 2688 |
. . 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 476 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐹) |
14 | 10, 12, 13 | sge0pnfval 39266 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = +∞) |
15 | | pnfel0pnf 38601 |
. . . . . 6
⊢ +∞
∈ (0[,]+∞) |
16 | 15 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈
(0[,]+∞)) |
17 | 14, 16 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) ∈ (0[,]+∞)) |
18 | 17 | adantlr 747 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) ∈ (0[,]+∞)) |
19 | | simpll 786 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran
𝐹) → 𝜑) |
20 | | neqne 2790 |
. . . . 5
⊢ (¬
𝐹 = ∅ → 𝐹 ≠ ∅) |
21 | 20 | ad2antlr 759 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹 ≠ ∅) |
22 | | simpr 476 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran
𝐹) → ¬ +∞
∈ ran 𝐹) |
23 | | 0xr 9965 |
. . . . . 6
⊢ 0 ∈
ℝ* |
24 | 23 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → 0 ∈
ℝ*) |
25 | | pnfxr 9971 |
. . . . . 6
⊢ +∞
∈ ℝ* |
26 | 25 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → +∞
∈ ℝ*) |
27 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝑋 ∈ 𝑉) |
28 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,]+∞)) |
29 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ¬ +∞
∈ ran 𝐹) |
30 | 28, 29 | fge0iccico 39263 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,)+∞)) |
31 | 27, 30 | sge0reval 39265 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
32 | | elinel2 3762 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin) |
33 | 32 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
34 | 11 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝐹:𝑋⟶(0[,]+∞)) |
35 | | elinel1 3761 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ 𝒫 𝑋) |
36 | | elpwi 4117 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑥 ⊆ 𝑋) |
40 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
41 | 39, 40 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
42 | 34, 41 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
43 | 42 | adantllr 751 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
44 | | nne 2786 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝐹‘𝑦) ≠ +∞ ↔ (𝐹‘𝑦) = +∞) |
45 | 44 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐹‘𝑦) ≠ +∞ → (𝐹‘𝑦) = +∞) |
46 | 45 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝐹‘𝑦) ≠ +∞ → +∞ = (𝐹‘𝑦)) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ ¬ (𝐹‘𝑦) ≠ +∞) → +∞ = (𝐹‘𝑦)) |
48 | | ffun 5961 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝑋⟶(0[,]+∞) → Fun 𝐹) |
49 | 11, 48 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Fun 𝐹) |
50 | 49 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → Fun 𝐹) |
51 | 41 | 3impa 1251 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
52 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹:𝑋⟶(0[,]+∞) → dom 𝐹 = 𝑋) |
53 | 11, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → dom 𝐹 = 𝑋) |
54 | 53 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 = dom 𝐹) |
55 | 54 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑋 = dom 𝐹) |
56 | 51, 55 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ dom 𝐹) |
57 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ ran 𝐹) |
58 | 50, 56, 57 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ran 𝐹) |
59 | 58 | ad5ant134 1305 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ ¬ (𝐹‘𝑦) ≠ +∞) → (𝐹‘𝑦) ∈ ran 𝐹) |
60 | 47, 59 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ ¬ (𝐹‘𝑦) ≠ +∞) → +∞ ∈ ran
𝐹) |
61 | 29 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ ¬ (𝐹‘𝑦) ≠ +∞) → ¬ +∞ ∈
ran 𝐹) |
62 | 60, 61 | condan 831 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ≠ +∞) |
63 | | ge0xrre 38605 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑦) ∈ (0[,]+∞) ∧ (𝐹‘𝑦) ≠ +∞) → (𝐹‘𝑦) ∈ ℝ) |
64 | 43, 62, 63 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℝ) |
65 | 33, 64 | fsumrecl 14312 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ℝ) |
66 | 65 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ℝ) |
67 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
68 | 67 | rnmptss 6299 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ℝ → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ) |
69 | 66, 68 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ) |
70 | | ressxr 9962 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ* |
71 | 70 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ℝ ⊆
ℝ*) |
72 | 69, 71 | sstrd 3578 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆
ℝ*) |
73 | | supxrcl 12017 |
. . . . . . . 8
⊢ (ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ* → sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) ∈
ℝ*) |
74 | 72, 73 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) ∈
ℝ*) |
75 | 31, 74 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) ∈
ℝ*) |
76 | 75 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) →
(Σ^‘𝐹) ∈
ℝ*) |
77 | 54 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → 𝑋 = dom 𝐹) |
78 | | neneq 2788 |
. . . . . . . . . . . 12
⊢ (𝐹 ≠ ∅ → ¬ 𝐹 = ∅) |
79 | 78 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → ¬ 𝐹 = ∅) |
80 | | frel 5963 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝑋⟶(0[,]+∞) → Rel 𝐹) |
81 | 11, 80 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Rel 𝐹) |
82 | 81 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → Rel 𝐹) |
83 | | reldm0 5264 |
. . . . . . . . . . . 12
⊢ (Rel
𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
85 | 79, 84 | mtbid 313 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → ¬ dom 𝐹 = ∅) |
86 | 85 | neqned 2789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → dom 𝐹 ≠ ∅) |
87 | 77, 86 | eqnetrd 2849 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → 𝑋 ≠ ∅) |
88 | | n0 3890 |
. . . . . . . 8
⊢ (𝑋 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝑋) |
89 | 87, 88 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ≠ ∅) → ∃𝑧 𝑧 ∈ 𝑋) |
90 | 89 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → ∃𝑧 𝑧 ∈ 𝑋) |
91 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → 0 ∈
ℝ*) |
92 | 11 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ (0[,]+∞)) |
93 | 92 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ (0[,]+∞)) |
94 | | nne 2786 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐹‘𝑧) ≠ +∞ ↔ (𝐹‘𝑧) = +∞) |
95 | 94 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝐹‘𝑧) ≠ +∞ → (𝐹‘𝑧) = +∞) |
96 | 95 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝐹‘𝑧) ≠ +∞ → +∞ = (𝐹‘𝑧)) |
97 | 96 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) ∧ ¬ (𝐹‘𝑧) ≠ +∞) → +∞ = (𝐹‘𝑧)) |
98 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
99 | 98, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → Fun 𝐹) |
100 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
101 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑋 = dom 𝐹) |
102 | 100, 101 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ dom 𝐹) |
103 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐹 ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ ran 𝐹) |
104 | 99, 102, 103 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ran 𝐹) |
105 | 104 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ran 𝐹) |
106 | 105 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) ∧ ¬ (𝐹‘𝑧) ≠ +∞) → (𝐹‘𝑧) ∈ ran 𝐹) |
107 | 97, 106 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) ∧ ¬ (𝐹‘𝑧) ≠ +∞) → +∞ ∈ ran
𝐹) |
108 | 29 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) ∧ ¬ (𝐹‘𝑧) ≠ +∞) → ¬ +∞ ∈
ran 𝐹) |
109 | 107, 108 | condan 831 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ≠ +∞) |
110 | | ge0xrre 38605 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ (0[,]+∞) ∧ (𝐹‘𝑧) ≠ +∞) → (𝐹‘𝑧) ∈ ℝ) |
111 | 93, 109, 110 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℝ) |
112 | 111 | rexrd 9968 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈
ℝ*) |
113 | 75 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) →
(Σ^‘𝐹) ∈
ℝ*) |
114 | 23 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 0 ∈
ℝ*) |
115 | 25 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → +∞ ∈
ℝ*) |
116 | | iccgelb 12101 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑧) ∈ (0[,]+∞)) → 0 ≤ (𝐹‘𝑧)) |
117 | 114, 115,
92, 116 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 0 ≤ (𝐹‘𝑧)) |
118 | 117 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → 0 ≤ (𝐹‘𝑧)) |
119 | 72 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆
ℝ*) |
120 | | snelpwi 4839 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑋 → {𝑧} ∈ 𝒫 𝑋) |
121 | | snfi 7923 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑧} ∈ Fin |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑋 → {𝑧} ∈ Fin) |
123 | 120, 122 | elind 3760 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑋 → {𝑧} ∈ (𝒫 𝑋 ∩ Fin)) |
124 | 123 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → {𝑧} ∈ (𝒫 𝑋 ∩ Fin)) |
125 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
126 | 111 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ) |
127 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) |
128 | 127 | sumsn 14319 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ ℂ) → Σ𝑦 ∈ {𝑧} (𝐹‘𝑦) = (𝐹‘𝑧)) |
129 | 125, 126,
128 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → Σ𝑦 ∈ {𝑧} (𝐹‘𝑦) = (𝐹‘𝑧)) |
130 | 129 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) = Σ𝑦 ∈ {𝑧} (𝐹‘𝑦)) |
131 | | sumeq1 14267 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = {𝑧} → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = Σ𝑦 ∈ {𝑧} (𝐹‘𝑦)) |
132 | 131 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = {𝑧} → ((𝐹‘𝑧) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ↔ (𝐹‘𝑧) = Σ𝑦 ∈ {𝑧} (𝐹‘𝑦))) |
133 | 132 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ (({𝑧} ∈ (𝒫 𝑋 ∩ Fin) ∧ (𝐹‘𝑧) = Σ𝑦 ∈ {𝑧} (𝐹‘𝑦)) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑧) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
134 | 124, 130,
133 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑧) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
135 | 67 | elrnmpt 5293 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑧) ∈ (0[,]+∞) → ((𝐹‘𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑧) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
136 | 93, 135 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐹‘𝑧) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
137 | 134, 136 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
138 | | supxrub 12026 |
. . . . . . . . . . . 12
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ* ∧ (𝐹‘𝑧) ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → (𝐹‘𝑧) ≤ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
139 | 119, 137,
138 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ≤ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
140 | 31 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) =
(Σ^‘𝐹)) |
141 | 140 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) =
(Σ^‘𝐹)) |
142 | 139, 141 | breqtrd 4609 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ≤
(Σ^‘𝐹)) |
143 | 91, 112, 113, 118, 142 | xrletrd 11869 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑧 ∈ 𝑋) → 0 ≤
(Σ^‘𝐹)) |
144 | 143 | ex 449 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → (𝑧 ∈ 𝑋 → 0 ≤
(Σ^‘𝐹))) |
145 | 144 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → (𝑧 ∈ 𝑋 → 0 ≤
(Σ^‘𝐹))) |
146 | 145 | exlimdv 1848 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → (∃𝑧 𝑧 ∈ 𝑋 → 0 ≤
(Σ^‘𝐹))) |
147 | 90, 146 | mpd 15 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) → 0 ≤
(Σ^‘𝐹)) |
148 | | pnfge 11840 |
. . . . . . 7
⊢
((Σ^‘𝐹) ∈ ℝ* →
(Σ^‘𝐹) ≤ +∞) |
149 | 75, 148 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) ≤ +∞) |
150 | 149 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) →
(Σ^‘𝐹) ≤ +∞) |
151 | 24, 26, 76, 147, 150 | eliccxrd 38600 |
. . . 4
⊢ (((𝜑 ∧ 𝐹 ≠ ∅) ∧ ¬ +∞ ∈
ran 𝐹) →
(Σ^‘𝐹) ∈ (0[,]+∞)) |
152 | 19, 21, 22, 151 | syl21anc 1317 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝐹 = ∅) ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) ∈ (0[,]+∞)) |
153 | 18, 152 | pm2.61dan 828 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐹 = ∅) →
(Σ^‘𝐹) ∈ (0[,]+∞)) |
154 | 8, 153 | pm2.61dan 828 |
1
⊢ (𝜑 →
(Σ^‘𝐹) ∈ (0[,]+∞)) |