| Step | Hyp | Ref
| Expression |
| 1 | | 0ex 5307 |
. . . . 5
⊢ ∅
∈ V |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ ∅ ∈ V) |
| 3 | | f0 6789 |
. . . . . 6
⊢
∅:∅⟶(0[,]+∞) |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ (⊤
→ ∅:∅⟶(0[,]+∞)) |
| 5 | | noel 4338 |
. . . . . . 7
⊢ ¬
+∞ ∈ ∅ |
| 6 | 5 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ¬ +∞ ∈ ∅) |
| 7 | | rn0 5936 |
. . . . . . . 8
⊢ ran
∅ = ∅ |
| 8 | 7 | eqcomi 2746 |
. . . . . . 7
⊢ ∅ =
ran ∅ |
| 9 | 8 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ∅ = ran ∅) |
| 10 | 6, 9 | neleqtrd 2863 |
. . . . 5
⊢ (⊤
→ ¬ +∞ ∈ ran ∅) |
| 11 | 4, 10 | fge0iccico 46385 |
. . . 4
⊢ (⊤
→ ∅:∅⟶(0[,)+∞)) |
| 12 | 2, 11 | sge0reval 46387 |
. . 3
⊢ (⊤
→ (Σ^‘∅) = sup(ran (𝑥 ∈ (𝒫 ∅ ∩
Fin) ↦ Σ𝑦
∈ 𝑥
(∅‘𝑦)),
ℝ*, < )) |
| 13 | 12 | mptru 1547 |
. 2
⊢
(Σ^‘∅) = sup(ran (𝑥 ∈ (𝒫 ∅ ∩
Fin) ↦ Σ𝑦
∈ 𝑥
(∅‘𝑦)),
ℝ*, < ) |
| 14 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
| 15 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝒫 ∅ ∩
Fin) ↦ Σ𝑦
∈ 𝑥
(∅‘𝑦)) = (𝑥 ∈ (𝒫 ∅ ∩
Fin) ↦ Σ𝑦
∈ 𝑥
(∅‘𝑦)) |
| 16 | 15 | elrnmpt 5969 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 ∅ ∩
Fin)𝑧 = Σ𝑦 ∈ 𝑥 (∅‘𝑦))) |
| 17 | 14, 16 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 ∅ ∩
Fin)𝑧 = Σ𝑦 ∈ 𝑥 (∅‘𝑦)) |
| 18 | 17 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) → ∃𝑥 ∈ (𝒫 ∅ ∩
Fin)𝑧 = Σ𝑦 ∈ 𝑥 (∅‘𝑦)) |
| 19 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑧 |
| 20 | | nfmpt1 5250 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) |
| 21 | 20 | nfrn 5963 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥ran
(𝑥 ∈ (𝒫
∅ ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (∅‘𝑦)) |
| 22 | 19, 21 | nfel 2920 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) |
| 23 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑧 = 0 |
| 24 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝒫 ∅ ∩
Fin) ∧ 𝑧 = Σ𝑦 ∈ 𝑥 (∅‘𝑦)) → 𝑧 = Σ𝑦 ∈ 𝑥 (∅‘𝑦)) |
| 25 | | elinel1 4201 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝒫 ∅ ∩
Fin) → 𝑥 ∈
𝒫 ∅) |
| 26 | | pw0 4812 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝒫
∅ = {∅} |
| 27 | 26 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝒫 ∅ ↔
𝑥 ∈
{∅}) |
| 28 | 27 | biimpi 216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝒫 ∅ →
𝑥 ∈
{∅}) |
| 29 | 25, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝒫 ∅ ∩
Fin) → 𝑥 ∈
{∅}) |
| 30 | | elsni 4643 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {∅} → 𝑥 = ∅) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 ∅ ∩
Fin) → 𝑥 =
∅) |
| 32 | 31 | sumeq1d 15736 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝒫 ∅ ∩
Fin) → Σ𝑦 ∈
𝑥 (∅‘𝑦) = Σ𝑦 ∈ ∅ (∅‘𝑦)) |
| 33 | 32 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝒫 ∅ ∩
Fin) ∧ 𝑧 = Σ𝑦 ∈ 𝑥 (∅‘𝑦)) → Σ𝑦 ∈ 𝑥 (∅‘𝑦) = Σ𝑦 ∈ ∅ (∅‘𝑦)) |
| 34 | | sum0 15757 |
. . . . . . . . . . . . . 14
⊢
Σ𝑦 ∈
∅ (∅‘𝑦) =
0 |
| 35 | 34 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (𝒫 ∅ ∩
Fin) ∧ 𝑧 = Σ𝑦 ∈ 𝑥 (∅‘𝑦)) → Σ𝑦 ∈ ∅ (∅‘𝑦) = 0) |
| 36 | 24, 33, 35 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝒫 ∅ ∩
Fin) ∧ 𝑧 = Σ𝑦 ∈ 𝑥 (∅‘𝑦)) → 𝑧 = 0) |
| 37 | 36 | ex 412 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝒫 ∅ ∩
Fin) → (𝑧 =
Σ𝑦 ∈ 𝑥 (∅‘𝑦) → 𝑧 = 0)) |
| 38 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) → (𝑥 ∈ (𝒫 ∅ ∩ Fin) →
(𝑧 = Σ𝑦 ∈ 𝑥 (∅‘𝑦) → 𝑧 = 0))) |
| 39 | 22, 23, 38 | rexlimd 3266 |
. . . . . . . . 9
⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) → (∃𝑥 ∈ (𝒫 ∅ ∩
Fin)𝑧 = Σ𝑦 ∈ 𝑥 (∅‘𝑦) → 𝑧 = 0)) |
| 40 | 18, 39 | mpd 15 |
. . . . . . . 8
⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) → 𝑧 = 0) |
| 41 | | velsn 4642 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {0} ↔ 𝑧 = 0) |
| 42 | 41 | bicomi 224 |
. . . . . . . . 9
⊢ (𝑧 = 0 ↔ 𝑧 ∈ {0}) |
| 43 | 42 | biimpi 216 |
. . . . . . . 8
⊢ (𝑧 = 0 → 𝑧 ∈ {0}) |
| 44 | 40, 43 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) → 𝑧 ∈ {0}) |
| 45 | | elsni 4643 |
. . . . . . . 8
⊢ (𝑧 ∈ {0} → 𝑧 = 0) |
| 46 | | 0elpw 5356 |
. . . . . . . . . . . . 13
⊢ ∅
∈ 𝒫 ∅ |
| 47 | | 0fi 9082 |
. . . . . . . . . . . . 13
⊢ ∅
∈ Fin |
| 48 | 46, 47 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (∅
∈ 𝒫 ∅ ∧ ∅ ∈ Fin) |
| 49 | | elin 3967 |
. . . . . . . . . . . 12
⊢ (∅
∈ (𝒫 ∅ ∩ Fin) ↔ (∅ ∈ 𝒫 ∅
∧ ∅ ∈ Fin)) |
| 50 | 48, 49 | mpbir 231 |
. . . . . . . . . . 11
⊢ ∅
∈ (𝒫 ∅ ∩ Fin) |
| 51 | 34 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ 0 =
Σ𝑦 ∈ ∅
(∅‘𝑦) |
| 52 | | sumeq1 15725 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → Σ𝑦 ∈ 𝑥 (∅‘𝑦) = Σ𝑦 ∈ ∅ (∅‘𝑦)) |
| 53 | 52 | rspceeqv 3645 |
. . . . . . . . . . 11
⊢ ((∅
∈ (𝒫 ∅ ∩ Fin) ∧ 0 = Σ𝑦 ∈ ∅ (∅‘𝑦)) → ∃𝑥 ∈ (𝒫 ∅ ∩
Fin)0 = Σ𝑦 ∈
𝑥 (∅‘𝑦)) |
| 54 | 50, 51, 53 | mp2an 692 |
. . . . . . . . . 10
⊢
∃𝑥 ∈
(𝒫 ∅ ∩ Fin)0 = Σ𝑦 ∈ 𝑥 (∅‘𝑦) |
| 55 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 56 | 15 | elrnmpt 5969 |
. . . . . . . . . . 11
⊢ (0 ∈
ℝ → (0 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 ∅ ∩
Fin)0 = Σ𝑦 ∈
𝑥 (∅‘𝑦))) |
| 57 | 55, 56 | ax-mp 5 |
. . . . . . . . . 10
⊢ (0 ∈
ran (𝑥 ∈ (𝒫
∅ ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (∅‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 ∅ ∩ Fin)0 =
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) |
| 58 | 54, 57 | mpbir 231 |
. . . . . . . . 9
⊢ 0 ∈
ran (𝑥 ∈ (𝒫
∅ ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (∅‘𝑦)) |
| 59 | 58 | a1i 11 |
. . . . . . . 8
⊢ (𝑧 ∈ {0} → 0 ∈ ran
(𝑥 ∈ (𝒫
∅ ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (∅‘𝑦))) |
| 60 | 45, 59 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝑧 ∈ {0} → 𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦))) |
| 61 | 44, 60 | impbii 209 |
. . . . . 6
⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) ↔ 𝑧 ∈ {0}) |
| 62 | 61 | ax-gen 1795 |
. . . . 5
⊢
∀𝑧(𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) ↔ 𝑧 ∈ {0}) |
| 63 | | dfcleq 2730 |
. . . . 5
⊢ (ran
(𝑥 ∈ (𝒫
∅ ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (∅‘𝑦)) = {0} ↔ ∀𝑧(𝑧 ∈ ran (𝑥 ∈ (𝒫 ∅ ∩ Fin) ↦
Σ𝑦 ∈ 𝑥 (∅‘𝑦)) ↔ 𝑧 ∈ {0})) |
| 64 | 62, 63 | mpbir 231 |
. . . 4
⊢ ran
(𝑥 ∈ (𝒫
∅ ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (∅‘𝑦)) = {0} |
| 65 | 64 | supeq1i 9487 |
. . 3
⊢ sup(ran
(𝑥 ∈ (𝒫
∅ ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (∅‘𝑦)), ℝ*, < ) = sup({0},
ℝ*, < ) |
| 66 | | xrltso 13183 |
. . . 4
⊢ < Or
ℝ* |
| 67 | | 0xr 11308 |
. . . 4
⊢ 0 ∈
ℝ* |
| 68 | | supsn 9512 |
. . . 4
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
| 69 | 66, 67, 68 | mp2an 692 |
. . 3
⊢ sup({0},
ℝ*, < ) = 0 |
| 70 | 65, 69 | eqtri 2765 |
. 2
⊢ sup(ran
(𝑥 ∈ (𝒫
∅ ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (∅‘𝑦)), ℝ*, < ) =
0 |
| 71 | 13, 70 | eqtri 2765 |
1
⊢
(Σ^‘∅) = 0 |