Step | Hyp | Ref
| Expression |
1 | | df-oms 30354 |
. . 3
⊢ toOMeas =
(𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)), (0[,]+∞), < ))) |
2 | 1 | a1i 11 |
. 2
⊢ (𝑅 ∈ V → toOMeas =
(𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)), (0[,]+∞), <
)))) |
3 | | dmeq 5324 |
. . . . . 6
⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅) |
4 | 3 | unieqd 4446 |
. . . . 5
⊢ (𝑟 = 𝑅 → ∪ dom
𝑟 = ∪ dom 𝑅) |
5 | 4 | pweqd 4163 |
. . . 4
⊢ (𝑟 = 𝑅 → 𝒫 ∪ dom 𝑟 = 𝒫 ∪ dom
𝑅) |
6 | 3 | pweqd 4163 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → 𝒫 dom 𝑟 = 𝒫 dom 𝑅) |
7 | | rabeq 3192 |
. . . . . . . 8
⊢
(𝒫 dom 𝑟 =
𝒫 dom 𝑅 →
{𝑧 ∈ 𝒫 dom
𝑟 ∣ (𝑎 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)} =
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝑎 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} = {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}) |
9 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑦 ∈ 𝑥) → 𝑟 = 𝑅) |
10 | 9 | fveq1d 6193 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑦 ∈ 𝑥) → (𝑟‘𝑦) = (𝑅‘𝑦)) |
11 | 10 | esumeq2dv 30100 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → Σ*𝑦 ∈ 𝑥(𝑟‘𝑦) = Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) |
12 | 8, 11 | mpteq12dv 4733 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦))) |
13 | 12 | rneqd 5353 |
. . . . 5
⊢ (𝑟 = 𝑅 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)) = ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦))) |
14 | 13 | infeq1d 8383 |
. . . 4
⊢ (𝑟 = 𝑅 → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)), (0[,]+∞), < ) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < )) |
15 | 5, 14 | mpteq12dv 4733 |
. . 3
⊢ (𝑟 = 𝑅 → (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)), (0[,]+∞), < )) = (𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < ))) |
16 | 15 | adantl 482 |
. 2
⊢ ((𝑅 ∈ V ∧ 𝑟 = 𝑅) → (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)), (0[,]+∞), < )) = (𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < ))) |
17 | | id 22 |
. 2
⊢ (𝑅 ∈ V → 𝑅 ∈ V) |
18 | | dmexg 7097 |
. . 3
⊢ (𝑅 ∈ V → dom 𝑅 ∈ V) |
19 | | uniexg 6955 |
. . 3
⊢ (dom
𝑅 ∈ V → ∪ dom 𝑅 ∈ V) |
20 | | pwexg 4850 |
. . 3
⊢ (∪ dom 𝑅 ∈ V → 𝒫 ∪ dom 𝑅 ∈ V) |
21 | | mptexg 6484 |
. . 3
⊢
(𝒫 ∪ dom 𝑅 ∈ V → (𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < )) ∈
V) |
22 | 18, 19, 20, 21 | 4syl 19 |
. 2
⊢ (𝑅 ∈ V → (𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < )) ∈
V) |
23 | 2, 16, 17, 22 | fvmptd 6288 |
1
⊢ (𝑅 ∈ V →
(toOMeas‘𝑅) = (𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < ))) |