Step |
Hyp |
Ref |
Expression |
1 |
|
nftru |
⊢ Ⅎ 𝑥 ⊤ |
2 |
|
nfcv |
⊢ Ⅎ 𝑥 ∅ |
3 |
|
0ex |
⊢ ∅ ∈ V |
4 |
3
|
a1i |
⊢ ( ⊤ → ∅ ∈ V ) |
5 |
|
ral0 |
⊢ ∀ 𝑥 ∈ ∅ 𝐴 ∈ ( 0 [,] +∞ ) |
6 |
5
|
a1i |
⊢ ( ⊤ → ∀ 𝑥 ∈ ∅ 𝐴 ∈ ( 0 [,] +∞ ) ) |
7 |
6
|
r19.21bi |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ∅ ) → 𝐴 ∈ ( 0 [,] +∞ ) ) |
8 |
|
pw0 |
⊢ 𝒫 ∅ = { ∅ } |
9 |
8
|
ineq1i |
⊢ ( 𝒫 ∅ ∩ Fin ) = ( { ∅ } ∩ Fin ) |
10 |
|
0fin |
⊢ ∅ ∈ Fin |
11 |
|
snssi |
⊢ ( ∅ ∈ Fin → { ∅ } ⊆ Fin ) |
12 |
|
df-ss |
⊢ ( { ∅ } ⊆ Fin ↔ ( { ∅ } ∩ Fin ) = { ∅ } ) |
13 |
11 12
|
sylib |
⊢ ( ∅ ∈ Fin → ( { ∅ } ∩ Fin ) = { ∅ } ) |
14 |
10 13
|
ax-mp |
⊢ ( { ∅ } ∩ Fin ) = { ∅ } |
15 |
9 14
|
eqtri |
⊢ ( 𝒫 ∅ ∩ Fin ) = { ∅ } |
16 |
15
|
eleq2i |
⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↔ 𝑦 ∈ { ∅ } ) |
17 |
|
velsn |
⊢ ( 𝑦 ∈ { ∅ } ↔ 𝑦 = ∅ ) |
18 |
16 17
|
sylbb |
⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑦 = ∅ ) |
19 |
18
|
mpteq1d |
⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) → ( 𝑥 ∈ 𝑦 ↦ 𝐴 ) = ( 𝑥 ∈ ∅ ↦ 𝐴 ) ) |
20 |
|
mpt0 |
⊢ ( 𝑥 ∈ ∅ ↦ 𝐴 ) = ∅ |
21 |
19 20
|
eqtrdi |
⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) → ( 𝑥 ∈ 𝑦 ↦ 𝐴 ) = ∅ ) |
22 |
21
|
oveq2d |
⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑥 ∈ 𝑦 ↦ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ∅ ) ) |
23 |
|
xrge00 |
⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) |
24 |
23
|
gsum0 |
⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ∅ ) = 0 |
25 |
22 24
|
eqtrdi |
⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑥 ∈ 𝑦 ↦ 𝐴 ) ) = 0 ) |
26 |
25
|
adantl |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑥 ∈ 𝑦 ↦ 𝐴 ) ) = 0 ) |
27 |
1 2 4 7 26
|
esumval |
⊢ ( ⊤ → Σ* 𝑥 ∈ ∅ 𝐴 = sup ( ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) , ℝ* , < ) ) |
28 |
27
|
mptru |
⊢ Σ* 𝑥 ∈ ∅ 𝐴 = sup ( ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) , ℝ* , < ) |
29 |
|
fconstmpt |
⊢ ( ( 𝒫 ∅ ∩ Fin ) × { 0 } ) = ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) |
30 |
29
|
eqcomi |
⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = ( ( 𝒫 ∅ ∩ Fin ) × { 0 } ) |
31 |
|
0xr |
⊢ 0 ∈ ℝ* |
32 |
31
|
rgenw |
⊢ ∀ 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) 0 ∈ ℝ* |
33 |
|
eqid |
⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) |
34 |
33
|
fnmpt |
⊢ ( ∀ 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) 0 ∈ ℝ* → ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) Fn ( 𝒫 ∅ ∩ Fin ) ) |
35 |
32 34
|
ax-mp |
⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) Fn ( 𝒫 ∅ ∩ Fin ) |
36 |
3
|
snnz |
⊢ { ∅ } ≠ ∅ |
37 |
15 36
|
eqnetri |
⊢ ( 𝒫 ∅ ∩ Fin ) ≠ ∅ |
38 |
|
fconst5 |
⊢ ( ( ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) Fn ( 𝒫 ∅ ∩ Fin ) ∧ ( 𝒫 ∅ ∩ Fin ) ≠ ∅ ) → ( ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = ( ( 𝒫 ∅ ∩ Fin ) × { 0 } ) ↔ ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = { 0 } ) ) |
39 |
35 37 38
|
mp2an |
⊢ ( ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = ( ( 𝒫 ∅ ∩ Fin ) × { 0 } ) ↔ ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = { 0 } ) |
40 |
30 39
|
mpbi |
⊢ ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = { 0 } |
41 |
40
|
supeq1i |
⊢ sup ( ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) , ℝ* , < ) = sup ( { 0 } , ℝ* , < ) |
42 |
|
xrltso |
⊢ < Or ℝ* |
43 |
|
supsn |
⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 ) |
44 |
42 31 43
|
mp2an |
⊢ sup ( { 0 } , ℝ* , < ) = 0 |
45 |
28 41 44
|
3eqtri |
⊢ Σ* 𝑥 ∈ ∅ 𝐴 = 0 |