Step | Hyp | Ref
| Expression |
1 | | oms.m |
. . 3
⊢ 𝑀 = (toOMeas‘𝑅) |
2 | 1 | fveq1i 6104 |
. 2
⊢ (𝑀‘∅) =
((toOMeas‘𝑅)‘∅) |
3 | | oms.o |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝑉) |
4 | | oms.r |
. . . 4
⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) |
5 | | 0ss 3924 |
. . . . 5
⊢ ∅
⊆ ∪ dom 𝑅 |
6 | | fdm 5964 |
. . . . . . 7
⊢ (𝑅:𝑄⟶(0[,]+∞) → dom 𝑅 = 𝑄) |
7 | 4, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝑅 = 𝑄) |
8 | 7 | unieqd 4382 |
. . . . 5
⊢ (𝜑 → ∪ dom 𝑅 = ∪ 𝑄) |
9 | 5, 8 | syl5sseq 3616 |
. . . 4
⊢ (𝜑 → ∅ ⊆ ∪ 𝑄) |
10 | | omsfval 29683 |
. . . 4
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∅ ⊆
∪ 𝑄) → ((toOMeas‘𝑅)‘∅) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < )) |
11 | 3, 4, 9, 10 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((toOMeas‘𝑅)‘∅) = inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < )) |
12 | | iccssxr 12127 |
. . . . . 6
⊢
(0[,]+∞) ⊆ ℝ* |
13 | | xrltso 11850 |
. . . . . 6
⊢ < Or
ℝ* |
14 | | soss 4977 |
. . . . . 6
⊢
((0[,]+∞) ⊆ ℝ* → ( < Or
ℝ* → < Or (0[,]+∞))) |
15 | 12, 13, 14 | mp2 9 |
. . . . 5
⊢ < Or
(0[,]+∞) |
16 | 15 | a1i 11 |
. . . 4
⊢ (𝜑 → < Or
(0[,]+∞)) |
17 | | 0e0iccpnf 12154 |
. . . . 5
⊢ 0 ∈
(0[,]+∞) |
18 | 17 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
(0[,]+∞)) |
19 | | oms.d |
. . . . . . . . . 10
⊢ (𝜑 → ∅ ∈ dom 𝑅) |
20 | 19 | snssd 4281 |
. . . . . . . . 9
⊢ (𝜑 → {∅} ⊆ dom
𝑅) |
21 | | p0ex 4779 |
. . . . . . . . . 10
⊢ {∅}
∈ V |
22 | 21 | elpw 4114 |
. . . . . . . . 9
⊢
({∅} ∈ 𝒫 dom 𝑅 ↔ {∅} ⊆ dom 𝑅) |
23 | 20, 22 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → {∅} ∈ 𝒫
dom 𝑅) |
24 | | 0ss 3924 |
. . . . . . . . 9
⊢ ∅
⊆ ∪ {∅} |
25 | | 0ex 4718 |
. . . . . . . . . 10
⊢ ∅
∈ V |
26 | | snct 28874 |
. . . . . . . . . 10
⊢ (∅
∈ V → {∅} ≼ ω) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . 9
⊢ {∅}
≼ ω |
28 | 24, 27 | pm3.2i 470 |
. . . . . . . 8
⊢ (∅
⊆ ∪ {∅} ∧ {∅} ≼
ω) |
29 | 23, 28 | jctir 559 |
. . . . . . 7
⊢ (𝜑 → ({∅} ∈
𝒫 dom 𝑅 ∧
(∅ ⊆ ∪ {∅} ∧ {∅} ≼
ω))) |
30 | | unieq 4380 |
. . . . . . . . . 10
⊢ (𝑧 = {∅} → ∪ 𝑧 =
∪ {∅}) |
31 | 30 | sseq2d 3596 |
. . . . . . . . 9
⊢ (𝑧 = {∅} → (∅
⊆ ∪ 𝑧 ↔ ∅ ⊆ ∪ {∅})) |
32 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑧 = {∅} → (𝑧 ≼ ω ↔
{∅} ≼ ω)) |
33 | 31, 32 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑧 = {∅} → ((∅
⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (∅ ⊆
∪ {∅} ∧ {∅} ≼
ω))) |
34 | 33 | elrab 3331 |
. . . . . . 7
⊢
({∅} ∈ {𝑧
∈ 𝒫 dom 𝑅
∣ (∅ ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ ({∅} ∈
𝒫 dom 𝑅 ∧
(∅ ⊆ ∪ {∅} ∧ {∅} ≼
ω))) |
35 | 29, 34 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → {∅} ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}) |
36 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = ∅) → 𝑦 = ∅) |
37 | 36 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝑅‘𝑦) = (𝑅‘∅)) |
38 | | oms.0 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅‘∅) = 0) |
39 | 38 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝑅‘∅) = 0) |
40 | 37, 39 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝑅‘𝑦) = 0) |
41 | 40, 19, 18 | esumsn 29454 |
. . . . . . 7
⊢ (𝜑 → Σ*𝑦 ∈ {∅} (𝑅‘𝑦) = 0) |
42 | 41 | eqcomd 2616 |
. . . . . 6
⊢ (𝜑 → 0 =
Σ*𝑦 ∈
{∅} (𝑅‘𝑦)) |
43 | | esumeq1 29423 |
. . . . . . . 8
⊢ (𝑥 = {∅} →
Σ*𝑦 ∈
𝑥(𝑅‘𝑦) = Σ*𝑦 ∈ {∅} (𝑅‘𝑦)) |
44 | 43 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑥 = {∅} → (0 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦) ↔ 0 = Σ*𝑦 ∈ {∅} (𝑅‘𝑦))) |
45 | 44 | rspcev 3282 |
. . . . . 6
⊢
(({∅} ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
∧ 0 = Σ*𝑦 ∈ {∅} (𝑅‘𝑦)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}0
= Σ*𝑦
∈ 𝑥(𝑅‘𝑦)) |
46 | 35, 42, 45 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}0
= Σ*𝑦
∈ 𝑥(𝑅‘𝑦)) |
47 | | 0xr 9965 |
. . . . . 6
⊢ 0 ∈
ℝ* |
48 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
49 | 48 | elrnmpt 5293 |
. . . . . 6
⊢ (0 ∈
ℝ* → (0 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}0
= Σ*𝑦
∈ 𝑥(𝑅‘𝑦))) |
50 | 47, 49 | ax-mp 5 |
. . . . 5
⊢ (0 ∈
ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}0
= Σ*𝑦
∈ 𝑥(𝑅‘𝑦)) |
51 | 46, 50 | sylibr 223 |
. . . 4
⊢ (𝜑 → 0 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) |
52 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑥𝜑 |
53 | | nfmpt1 4675 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
54 | 53 | nfrn 5289 |
. . . . . . . . 9
⊢
Ⅎ𝑥ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
55 | 54 | nfcri 2745 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
56 | 52, 55 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) |
57 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) → 𝑎 = Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
58 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
59 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝜑 |
60 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦{𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)} |
61 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦𝑥 |
62 | 61 | nfesum1 29429 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦Σ*𝑦 ∈ 𝑥(𝑅‘𝑦) |
63 | 60, 62 | nfmpt 4674 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
64 | 63 | nfrn 5289 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
65 | 64 | nfcri 2745 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
66 | 59, 65 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) |
67 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)} |
68 | 66, 67 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}) |
69 | 62 | nfeq2 2766 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑎 = Σ*𝑦 ∈ 𝑥(𝑅‘𝑦) |
70 | 68, 69 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) |
71 | 4 | ad4antr 764 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑅:𝑄⟶(0[,]+∞)) |
72 | | ssrab2 3650 |
. . . . . . . . . . . . . . . 16
⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
⊆ 𝒫 dom 𝑅 |
73 | | simpllr 795 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}) |
74 | 72, 73 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝒫 dom 𝑅) |
75 | 7 | pweqd 4113 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝒫 dom 𝑅 = 𝒫 𝑄) |
76 | 75 | ad4antr 764 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝒫 dom 𝑅 = 𝒫 𝑄) |
77 | 74, 76 | eleqtrd 2690 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝑄) |
78 | 77 | elpwid 4118 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑥 ⊆ 𝑄) |
79 | | simpr 476 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
80 | 78, 79 | sseldd 3569 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑄) |
81 | 71, 80 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) ∧ 𝑦 ∈ 𝑥) → (𝑅‘𝑦) ∈ (0[,]+∞)) |
82 | 81 | ex 449 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) → (𝑦 ∈ 𝑥 → (𝑅‘𝑦) ∈ (0[,]+∞))) |
83 | 70, 82 | ralrimi 2940 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) → ∀𝑦 ∈ 𝑥 (𝑅‘𝑦) ∈ (0[,]+∞)) |
84 | 61 | esumcl 29419 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (𝑅‘𝑦) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑥(𝑅‘𝑦) ∈ (0[,]+∞)) |
85 | 58, 83, 84 | sylancr 694 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) → Σ*𝑦 ∈ 𝑥(𝑅‘𝑦) ∈ (0[,]+∞)) |
86 | 57, 85 | eqeltrd 2688 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) ∧ 𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)})
∧ 𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) → 𝑎 ∈ (0[,]+∞)) |
87 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑎 ∈ V |
88 | 48 | elrnmpt 5293 |
. . . . . . . . . 10
⊢ (𝑎 ∈ V → (𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦))) |
89 | 87, 88 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) |
90 | 89 | biimpi 205 |
. . . . . . . 8
⊢ (𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) |
91 | 90 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}𝑎 =
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) |
92 | 56, 86, 91 | r19.29af 3058 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → 𝑎 ∈ (0[,]+∞)) |
93 | | pnfxr 9971 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
94 | | iccgelb 12101 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
𝑎 ∈ (0[,]+∞))
→ 0 ≤ 𝑎) |
95 | 47, 93, 94 | mp3an12 1406 |
. . . . . 6
⊢ (𝑎 ∈ (0[,]+∞) → 0
≤ 𝑎) |
96 | 92, 95 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → 0 ≤ 𝑎) |
97 | 12, 92 | sseldi 3566 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → 𝑎 ∈ ℝ*) |
98 | | xrlenlt 9982 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ 𝑎 ∈ ℝ*) → (0 ≤
𝑎 ↔ ¬ 𝑎 < 0)) |
99 | 98 | bicomd 212 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ 𝑎 ∈ ℝ*) → (¬
𝑎 < 0 ↔ 0 ≤
𝑎)) |
100 | 47, 97, 99 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → (¬ 𝑎 < 0 ↔ 0 ≤ 𝑎)) |
101 | 96, 100 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦))) → ¬ 𝑎 < 0) |
102 | 16, 18, 51, 101 | infmin 8283 |
. . 3
⊢ (𝜑 → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∅ ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < ) =
0) |
103 | 11, 102 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((toOMeas‘𝑅)‘∅) =
0) |
104 | 2, 103 | syl5eq 2656 |
1
⊢ (𝜑 → (𝑀‘∅) = 0) |