Step | Hyp | Ref
| Expression |
1 | | snex 4835 |
. . . . 5
⊢ {𝐴} ∈ V |
2 | 1 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐴) = +∞) → {𝐴} ∈ V) |
3 | | sge0sn.2 |
. . . . 5
⊢ (𝜑 → 𝐹:{𝐴}⟶(0[,]+∞)) |
4 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐴) = +∞) → 𝐹:{𝐴}⟶(0[,]+∞)) |
5 | | id 22 |
. . . . . . 7
⊢ ((𝐹‘𝐴) = +∞ → (𝐹‘𝐴) = +∞) |
6 | 5 | eqcomd 2616 |
. . . . . 6
⊢ ((𝐹‘𝐴) = +∞ → +∞ = (𝐹‘𝐴)) |
7 | 6 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐴) = +∞) → +∞ = (𝐹‘𝐴)) |
8 | | ffun 5961 |
. . . . . . . 8
⊢ (𝐹:{𝐴}⟶(0[,]+∞) → Fun 𝐹) |
9 | 3, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Fun 𝐹) |
10 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐴) = +∞) → Fun 𝐹) |
11 | | sge0sn.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
12 | | snidg 4153 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
14 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝐹:{𝐴}⟶(0[,]+∞) → dom 𝐹 = {𝐴}) |
15 | 3, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = {𝐴}) |
16 | 15 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝜑 → {𝐴} = dom 𝐹) |
17 | 13, 16 | eleqtrd 2690 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ dom 𝐹) |
18 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐴) = +∞) → 𝐴 ∈ dom 𝐹) |
19 | | fvelrn 6260 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) |
20 | 10, 18, 19 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐴) = +∞) → (𝐹‘𝐴) ∈ ran 𝐹) |
21 | 7, 20 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐴) = +∞) → +∞ ∈ ran
𝐹) |
22 | 2, 4, 21 | sge0pnfval 39266 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐴) = +∞) →
(Σ^‘𝐹) = +∞) |
23 | | simpr 476 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐴) = +∞) → (𝐹‘𝐴) = +∞) |
24 | 22, 23 | eqtr4d 2647 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝐴) = +∞) →
(Σ^‘𝐹) = (𝐹‘𝐴)) |
25 | 1 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → {𝐴} ∈ V) |
26 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → 𝐹:{𝐴}⟶(0[,]+∞)) |
27 | | elsni 4142 |
. . . . . . . . 9
⊢ (+∞
∈ {(𝐹‘𝐴)} → +∞ = (𝐹‘𝐴)) |
28 | 27 | eqcomd 2616 |
. . . . . . . 8
⊢ (+∞
∈ {(𝐹‘𝐴)} → (𝐹‘𝐴) = +∞) |
29 | 28 | con3i 149 |
. . . . . . 7
⊢ (¬
(𝐹‘𝐴) = +∞ → ¬ +∞ ∈
{(𝐹‘𝐴)}) |
30 | 29 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → ¬ +∞ ∈
{(𝐹‘𝐴)}) |
31 | 11, 3 | rnsnf 38365 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 = {(𝐹‘𝐴)}) |
32 | 31 | eqcomd 2616 |
. . . . . . 7
⊢ (𝜑 → {(𝐹‘𝐴)} = ran 𝐹) |
33 | 32 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → {(𝐹‘𝐴)} = ran 𝐹) |
34 | 30, 33 | neleqtrd 2709 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → ¬ +∞ ∈
ran 𝐹) |
35 | 26, 34 | fge0iccico 39263 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → 𝐹:{𝐴}⟶(0[,)+∞)) |
36 | 25, 35 | sge0reval 39265 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
37 | | sum0 14299 |
. . . . . . . 8
⊢
Σ𝑦 ∈
∅ (𝐹‘𝑦) = 0 |
38 | 37 | eqcomi 2619 |
. . . . . . 7
⊢ 0 =
Σ𝑦 ∈ ∅
(𝐹‘𝑦) |
39 | 38 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → 0 = Σ𝑦 ∈ ∅ (𝐹‘𝑦)) |
40 | | nfcvd 2752 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → Ⅎ𝑦(𝐹‘𝐴)) |
41 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) |
42 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝐹‘𝑦) = (𝐹‘𝐴)) |
43 | 42 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) ∧ 𝑦 = 𝐴) → (𝐹‘𝑦) = (𝐹‘𝐴)) |
44 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → 𝐴 ∈ 𝑉) |
45 | | rge0ssre 12151 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
46 | | ax-resscn 9872 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
47 | 45, 46 | sstri 3577 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℂ |
48 | 44, 12 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → 𝐴 ∈ {𝐴}) |
49 | 35, 48 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → (𝐹‘𝐴) ∈ (0[,)+∞)) |
50 | 47, 49 | sseldi 3566 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → (𝐹‘𝐴) ∈ ℂ) |
51 | 40, 41, 43, 44, 50 | sumsnd 38208 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → Σ𝑦 ∈ {𝐴} (𝐹‘𝑦) = (𝐹‘𝐴)) |
52 | 51 | eqcomd 2616 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → (𝐹‘𝐴) = Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)) |
53 | 39, 52 | preq12d 4220 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → {0, (𝐹‘𝐴)} = {Σ𝑦 ∈ ∅ (𝐹‘𝑦), Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)}) |
54 | 53 | supeq1d 8235 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → sup({0, (𝐹‘𝐴)}, ℝ*, < ) =
sup({Σ𝑦 ∈
∅ (𝐹‘𝑦), Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)}, ℝ*, <
)) |
55 | | xrltso 11850 |
. . . . . . . 8
⊢ < Or
ℝ* |
56 | 55 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → < Or
ℝ*) |
57 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
58 | 57 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ*) |
59 | | iccssxr 12127 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
60 | 3, 13 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐴) ∈ (0[,]+∞)) |
61 | 59, 60 | sseldi 3566 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐴) ∈
ℝ*) |
62 | | suppr 8260 |
. . . . . . 7
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ* ∧ (𝐹‘𝐴) ∈ ℝ*) → sup({0,
(𝐹‘𝐴)}, ℝ*, < ) = if((𝐹‘𝐴) < 0, 0, (𝐹‘𝐴))) |
63 | 56, 58, 61, 62 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → sup({0, (𝐹‘𝐴)}, ℝ*, < ) = if((𝐹‘𝐴) < 0, 0, (𝐹‘𝐴))) |
64 | | pnfxr 9971 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
65 | 64 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → +∞ ∈
ℝ*) |
66 | 58, 65, 60 | 3jca 1235 |
. . . . . . . . 9
⊢ (𝜑 → (0 ∈
ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹‘𝐴) ∈ (0[,]+∞))) |
67 | | iccgelb 12101 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝐴) ∈ (0[,]+∞)) → 0 ≤
(𝐹‘𝐴)) |
68 | 66, 67 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (𝐹‘𝐴)) |
69 | 58, 61 | xrlenltd 9983 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (𝐹‘𝐴) ↔ ¬ (𝐹‘𝐴) < 0)) |
70 | 68, 69 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝐹‘𝐴) < 0) |
71 | 70 | iffalsed 4047 |
. . . . . 6
⊢ (𝜑 → if((𝐹‘𝐴) < 0, 0, (𝐹‘𝐴)) = (𝐹‘𝐴)) |
72 | 63, 71 | eqtr2d 2645 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) = sup({0, (𝐹‘𝐴)}, ℝ*, <
)) |
73 | 72 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → (𝐹‘𝐴) = sup({0, (𝐹‘𝐴)}, ℝ*, <
)) |
74 | | pwsn 4366 |
. . . . . . . . . . . 12
⊢ 𝒫
{𝐴} = {∅, {𝐴}} |
75 | 74 | ineq1i 3772 |
. . . . . . . . . . 11
⊢
(𝒫 {𝐴} ∩
Fin) = ({∅, {𝐴}}
∩ Fin) |
76 | | 0fin 8073 |
. . . . . . . . . . . . 13
⊢ ∅
∈ Fin |
77 | | snfi 7923 |
. . . . . . . . . . . . 13
⊢ {𝐴} ∈ Fin |
78 | | prssi 4293 |
. . . . . . . . . . . . 13
⊢ ((∅
∈ Fin ∧ {𝐴} ∈
Fin) → {∅, {𝐴}}
⊆ Fin) |
79 | 76, 77, 78 | mp2an 704 |
. . . . . . . . . . . 12
⊢ {∅,
{𝐴}} ⊆
Fin |
80 | | df-ss 3554 |
. . . . . . . . . . . . 13
⊢
({∅, {𝐴}}
⊆ Fin ↔ ({∅, {𝐴}} ∩ Fin) = {∅, {𝐴}}) |
81 | 80 | biimpi 205 |
. . . . . . . . . . . 12
⊢
({∅, {𝐴}}
⊆ Fin → ({∅, {𝐴}} ∩ Fin) = {∅, {𝐴}}) |
82 | 79, 81 | ax-mp 5 |
. . . . . . . . . . 11
⊢
({∅, {𝐴}}
∩ Fin) = {∅, {𝐴}} |
83 | 75, 82 | eqtri 2632 |
. . . . . . . . . 10
⊢
(𝒫 {𝐴} ∩
Fin) = {∅, {𝐴}} |
84 | | mpteq1 4665 |
. . . . . . . . . 10
⊢
((𝒫 {𝐴}
∩ Fin) = {∅, {𝐴}}
→ (𝑥 ∈ (𝒫
{𝐴} ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ {∅, {𝐴}} ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
85 | 83, 84 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ {∅, {𝐴}} ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
86 | | 0ex 4718 |
. . . . . . . . . . . . 13
⊢ ∅
∈ V |
87 | 86 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ ∅ ∈ V) |
88 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ {𝐴} ∈
V) |
89 | | sumex 14266 |
. . . . . . . . . . . . 13
⊢
Σ𝑦 ∈
∅ (𝐹‘𝑦) ∈ V |
90 | 89 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ Σ𝑦 ∈
∅ (𝐹‘𝑦) ∈ V) |
91 | | sumex 14266 |
. . . . . . . . . . . . 13
⊢
Σ𝑦 ∈
{𝐴} (𝐹‘𝑦) ∈ V |
92 | 91 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ Σ𝑦 ∈
{𝐴} (𝐹‘𝑦) ∈ V) |
93 | | sumeq1 14267 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = Σ𝑦 ∈ ∅ (𝐹‘𝑦)) |
94 | 93 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥 =
∅) → Σ𝑦
∈ 𝑥 (𝐹‘𝑦) = Σ𝑦 ∈ ∅ (𝐹‘𝑦)) |
95 | | sumeq1 14267 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {𝐴} → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)) |
96 | 95 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥 =
{𝐴}) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)) |
97 | 87, 88, 90, 92, 94, 96 | fmptpr 6343 |
. . . . . . . . . . 11
⊢ (⊤
→ {〈∅, Σ𝑦 ∈ ∅ (𝐹‘𝑦)〉, 〈{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)〉} = (𝑥 ∈ {∅, {𝐴}} ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
98 | 97 | trud 1484 |
. . . . . . . . . 10
⊢
{〈∅, Σ𝑦 ∈ ∅ (𝐹‘𝑦)〉, 〈{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)〉} = (𝑥 ∈ {∅, {𝐴}} ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
99 | 98 | eqcomi 2619 |
. . . . . . . . 9
⊢ (𝑥 ∈ {∅, {𝐴}} ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = {〈∅, Σ𝑦 ∈ ∅ (𝐹‘𝑦)〉, 〈{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)〉} |
100 | 85, 99 | eqtri 2632 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = {〈∅, Σ𝑦 ∈ ∅ (𝐹‘𝑦)〉, 〈{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)〉} |
101 | 100 | rneqi 5273 |
. . . . . . 7
⊢ ran
(𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = ran {〈∅, Σ𝑦 ∈ ∅ (𝐹‘𝑦)〉, 〈{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)〉} |
102 | | rnpropg 5533 |
. . . . . . . 8
⊢ ((∅
∈ V ∧ {𝐴} ∈
V) → ran {〈∅, Σ𝑦 ∈ ∅ (𝐹‘𝑦)〉, 〈{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)〉} = {Σ𝑦 ∈ ∅ (𝐹‘𝑦), Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)}) |
103 | 86, 1, 102 | mp2an 704 |
. . . . . . 7
⊢ ran
{〈∅, Σ𝑦
∈ ∅ (𝐹‘𝑦)〉, 〈{𝐴}, Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)〉} = {Σ𝑦 ∈ ∅ (𝐹‘𝑦), Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)} |
104 | 101, 103 | eqtri 2632 |
. . . . . 6
⊢ ran
(𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = {Σ𝑦 ∈ ∅ (𝐹‘𝑦), Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)} |
105 | 104 | supeq1i 8236 |
. . . . 5
⊢ sup(ran
(𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) =
sup({Σ𝑦 ∈
∅ (𝐹‘𝑦), Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)}, ℝ*, <
) |
106 | 105 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → sup(ran (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) =
sup({Σ𝑦 ∈
∅ (𝐹‘𝑦), Σ𝑦 ∈ {𝐴} (𝐹‘𝑦)}, ℝ*, <
)) |
107 | 54, 73, 106 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) → (𝐹‘𝐴) = sup(ran (𝑥 ∈ (𝒫 {𝐴} ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
108 | 36, 107 | eqtr4d 2647 |
. 2
⊢ ((𝜑 ∧ ¬ (𝐹‘𝐴) = +∞) →
(Σ^‘𝐹) = (𝐹‘𝐴)) |
109 | 24, 108 | pm2.61dan 828 |
1
⊢ (𝜑 →
(Σ^‘𝐹) = (𝐹‘𝐴)) |