| Step | Hyp | Ref
| Expression |
| 1 | | oms.m |
. . 3
⊢ 𝑀 = (toOMeas‘𝑅) |
| 2 | 1 | fveq1i 6907 |
. 2
⊢ (𝑀‘∅) =
((toOMeas‘𝑅)‘∅) |
| 3 | | oms.o |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝑉) |
| 4 | | oms.r |
. . . 4
⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) |
| 5 | | 0ss 4400 |
. . . . 5
⊢ ∅
⊆ ∪ dom 𝑅 |
| 6 | 4 | fdmd 6746 |
. . . . . 6
⊢ (𝜑 → dom 𝑅 = 𝑄) |
| 7 | 6 | unieqd 4920 |
. . . . 5
⊢ (𝜑 → ∪ dom 𝑅 = ∪ 𝑄) |
| 8 | 5, 7 | sseqtrid 4026 |
. . . 4
⊢ (𝜑 → ∅ ⊆ ∪ 𝑄) |
| 9 | | omsfval 34296 |
. . . 4
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∅ ⊆
∪ 𝑄) → ((toOMeas‘𝑅)‘∅) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < )) |
| 10 | 3, 4, 8, 9 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((toOMeas‘𝑅)‘∅) = inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < )) |
| 11 | | iccssxr 13470 |
. . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* |
| 12 | | xrltso 13183 |
. . . . . 6
⊢ < Or
ℝ* |
| 13 | | soss 5612 |
. . . . . 6
⊢
((0[,]+∞) ⊆ ℝ* → ( < Or
ℝ* → < Or (0[,]+∞))) |
| 14 | 11, 12, 13 | mp2 9 |
. . . . 5
⊢ < Or
(0[,]+∞) |
| 15 | 14 | a1i 11 |
. . . 4
⊢ (𝜑 → < Or
(0[,]+∞)) |
| 16 | | 0e0iccpnf 13499 |
. . . . 5
⊢ 0 ∈
(0[,]+∞) |
| 17 | 16 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
(0[,]+∞)) |
| 18 | | oms.d |
. . . . . . . . . 10
⊢ (𝜑 → ∅ ∈ dom 𝑅) |
| 19 | 18 | snssd 4809 |
. . . . . . . . 9
⊢ (𝜑 → {∅} ⊆ dom
𝑅) |
| 20 | | p0ex 5384 |
. . . . . . . . . 10
⊢ {∅}
∈ V |
| 21 | 20 | elpw 4604 |
. . . . . . . . 9
⊢
({∅} ∈ 𝒫 dom 𝑅 ↔ {∅} ⊆ dom 𝑅) |
| 22 | 19, 21 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → {∅} ∈ 𝒫
dom 𝑅) |
| 23 | | 0ss 4400 |
. . . . . . . . 9
⊢ ∅
⊆ ∪ {∅} |
| 24 | | 0ex 5307 |
. . . . . . . . . 10
⊢ ∅
∈ V |
| 25 | | snct 32725 |
. . . . . . . . . 10
⊢ (∅
∈ V → {∅} ≼ ω) |
| 26 | 24, 25 | ax-mp 5 |
. . . . . . . . 9
⊢ {∅}
≼ ω |
| 27 | 23, 26 | pm3.2i 470 |
. . . . . . . 8
⊢ (∅
⊆ ∪ {∅} ∧ {∅} ≼
ω) |
| 28 | 22, 27 | jctir 520 |
. . . . . . 7
⊢ (𝜑 → ({∅} ∈
𝒫 dom 𝑅 ∧
(∅ ⊆ ∪ {∅} ∧ {∅} ≼
ω))) |
| 29 | | unieq 4918 |
. . . . . . . . . 10
⊢ (𝑧 = {∅} → ∪ 𝑧 =
∪ {∅}) |
| 30 | 29 | sseq2d 4016 |
. . . . . . . . 9
⊢ (𝑧 = {∅} → (∅
⊆ ∪ 𝑧 ↔ ∅ ⊆ ∪ {∅})) |
| 31 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑧 = {∅} → (𝑧 ≼ ω ↔
{∅} ≼ ω)) |
| 32 | 30, 31 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑧 = {∅} → ((∅
⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (∅ ⊆
∪ {∅} ∧ {∅} ≼
ω))) |
| 33 | 32 | elrab 3692 |
. . . . . . 7
⊢
({∅} ∈ {𝑧
∈ 𝒫 dom 𝑅
∣ (∅ ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ ({∅} ∈
𝒫 dom 𝑅 ∧
(∅ ⊆ ∪ {∅} ∧ {∅} ≼
ω))) |
| 34 | 28, 33 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → {∅} ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}) |
| 35 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = ∅) → 𝑦 = ∅) |
| 36 | 35 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝑅‘𝑦) = (𝑅‘∅)) |
| 37 | | oms.0 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅‘∅) = 0) |
| 38 | 37 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝑅‘∅) = 0) |
| 39 | 36, 38 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝑅‘𝑦) = 0) |
| 40 | 39, 18, 17 | esumsn 34066 |
. . . . . . 7
⊢ (𝜑 → Σ*𝑦 ∈ {∅} (𝑅‘𝑦) = 0) |
| 41 | 40 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → 0 =
Σ*𝑦 ∈
{∅} (𝑅‘𝑦)) |
| 42 | | esumeq1 34035 |
. . . . . . 7
⊢ (𝑥 = {∅} →
Σ*𝑦 ∈
𝑥(𝑅‘𝑦) = Σ*𝑦 ∈ {∅} (𝑅‘𝑦)) |
| 43 | 42 | rspceeqv 3645 |
. . . . . 6
⊢
(({∅} ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
∧ 0 = Σ*𝑦 ∈ {∅} (𝑅‘𝑦)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}0
= Σ*𝑦
∈ 𝑥(𝑅‘𝑦)) |
| 44 | 34, 41, 43 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}0
= Σ*𝑦
∈ 𝑥(𝑅‘𝑦)) |
| 45 | | 0xr 11308 |
. . . . . 6
⊢ 0 ∈
ℝ* |
| 46 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
| 47 | 46 | elrnmpt 5969 |
. . . . . 6
⊢ (0 ∈
ℝ* → (0 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}0
= Σ*𝑦
∈ 𝑥(𝑅‘𝑦))) |
| 48 | 45, 47 | ax-mp 5 |
. . . . 5
⊢ (0 ∈
ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}0
= Σ*𝑦
∈ 𝑥(𝑅‘𝑦)) |
| 49 | 44, 48 | sylibr 234 |
. . . 4
⊢ (𝜑 → 0 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) |
| 50 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥𝜑 |
| 51 | | nfmpt1 5250 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
| 52 | 51 | nfrn 5963 |
. . . . . . . . 9
⊢
Ⅎ𝑥ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
| 53 | 52 | nfcri 2897 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
| 54 | 50, 53 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) |
| 55 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) → 𝑎 = Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
| 56 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 57 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝜑 |
| 58 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦{𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)} |
| 59 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦𝑥 |
| 60 | 59 | nfesum1 34041 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦Σ*𝑦 ∈ 𝑥(𝑅‘𝑦) |
| 61 | 58, 60 | nfmpt 5249 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
| 62 | 61 | nfrn 5963 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
| 63 | 62 | nfcri 2897 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
| 64 | 57, 63 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) |
| 65 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)} |
| 66 | 64, 65 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}) |
| 67 | 60 | nfeq2 2923 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑎 = Σ*𝑦 ∈ 𝑥(𝑅‘𝑦) |
| 68 | 66, 67 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) |
| 69 | 4 | ad4antr 732 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑅:𝑄⟶(0[,]+∞)) |
| 70 | | ssrab2 4080 |
. . . . . . . . . . . . . . . 16
⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
⊆ 𝒫 dom 𝑅 |
| 71 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}) |
| 72 | 70, 71 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝒫 dom 𝑅) |
| 73 | 6 | pweqd 4617 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝒫 dom 𝑅 = 𝒫 𝑄) |
| 74 | 73 | ad4antr 732 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝒫 dom 𝑅 = 𝒫 𝑄) |
| 75 | 72, 74 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝑄) |
| 76 | 75 | elpwid 4609 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑥 ⊆ 𝑄) |
| 77 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
| 78 | 76, 77 | sseldd 3984 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑄) |
| 79 | 69, 78 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → (𝑅‘𝑦) ∈ (0[,]+∞)) |
| 80 | 79 | ex 412 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) → (𝑦 ∈ 𝑥 → (𝑅‘𝑦) ∈ (0[,]+∞))) |
| 81 | 68, 80 | ralrimi 3257 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) → ∀𝑦 ∈ 𝑥 (𝑅‘𝑦) ∈ (0[,]+∞)) |
| 82 | 59 | esumcl 34031 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (𝑅‘𝑦) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑥(𝑅‘𝑦) ∈ (0[,]+∞)) |
| 83 | 56, 81, 82 | sylancr 587 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) → Σ*𝑦 ∈ 𝑥(𝑅‘𝑦) ∈ (0[,]+∞)) |
| 84 | 55, 83 | eqeltrd 2841 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) → 𝑎 ∈ (0[,]+∞)) |
| 85 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
| 86 | 46 | elrnmpt 5969 |
. . . . . . . . . 10
⊢ (𝑎 ∈ V → (𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦))) |
| 87 | 85, 86 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) |
| 88 | 87 | biimpi 216 |
. . . . . . . 8
⊢ (𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) |
| 89 | 88 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) |
| 90 | 54, 84, 89 | r19.29af 3268 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → 𝑎 ∈ (0[,]+∞)) |
| 91 | | pnfxr 11315 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
| 92 | | iccgelb 13443 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝑎 ∈ (0[,]+∞))
→ 0 ≤ 𝑎) |
| 93 | 45, 91, 92 | mp3an12 1453 |
. . . . . 6
⊢ (𝑎 ∈ (0[,]+∞) → 0
≤ 𝑎) |
| 94 | 90, 93 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → 0 ≤ 𝑎) |
| 95 | 11, 90 | sselid 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → 𝑎 ∈ ℝ*) |
| 96 | | xrlenlt 11326 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ 𝑎 ∈ ℝ*) → (0 ≤
𝑎 ↔ ¬ 𝑎 < 0)) |
| 97 | 96 | bicomd 223 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ 𝑎 ∈ ℝ*) → (¬
𝑎 < 0 ↔ 0 ≤
𝑎)) |
| 98 | 45, 95, 97 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → (¬ 𝑎 < 0 ↔ 0 ≤ 𝑎)) |
| 99 | 94, 98 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → ¬ 𝑎 < 0) |
| 100 | 15, 17, 49, 99 | infmin 9534 |
. . 3
⊢ (𝜑 → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < ) =
0) |
| 101 | 10, 100 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((toOMeas‘𝑅)‘∅) =
0) |
| 102 | 2, 101 | eqtrid 2789 |
1
⊢ (𝜑 → (𝑀‘∅) = 0) |