Step | Hyp | Ref
| Expression |
1 | | simp2 1128 |
. . . 4
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ 𝑅:𝑄⟶(0[,]+∞)) |
2 | | simp1 1127 |
. . . 4
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ 𝑄 ∈ 𝑉) |
3 | | fex 6763 |
. . . 4
⊢ ((𝑅:𝑄⟶(0[,]+∞) ∧ 𝑄 ∈ 𝑉) → 𝑅 ∈ V) |
4 | 1, 2, 3 | syl2anc 579 |
. . 3
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ 𝑅 ∈
V) |
5 | | omsval 30957 |
. . 3
⊢ (𝑅 ∈ V →
(toOMeas‘𝑅) = (𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < ))) |
6 | 4, 5 | syl 17 |
. 2
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ (toOMeas‘𝑅) =
(𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < ))) |
7 | | simpr 479 |
. . . . . . . 8
⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
∧ 𝑎 = 𝐴) → 𝑎 = 𝐴) |
8 | 7 | sseq1d 3851 |
. . . . . . 7
⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
∧ 𝑎 = 𝐴) → (𝑎 ⊆ ∪ 𝑧 ↔ 𝐴 ⊆ ∪ 𝑧)) |
9 | 8 | anbi1d 623 |
. . . . . 6
⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
∧ 𝑎 = 𝐴) → ((𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω))) |
10 | 9 | rabbidv 3386 |
. . . . 5
⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
∧ 𝑎 = 𝐴) → {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} = {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}) |
11 | 10 | mpteq1d 4975 |
. . . 4
⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
∧ 𝑎 = 𝐴) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦))) |
12 | 11 | rneqd 5600 |
. . 3
⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
∧ 𝑎 = 𝐴) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)) = ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦))) |
13 | 12 | infeq1d 8673 |
. 2
⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
∧ 𝑎 = 𝐴) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < ) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < )) |
14 | | simp3 1129 |
. . . 4
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ 𝐴 ⊆ ∪ 𝑄) |
15 | | fdm 6301 |
. . . . . 6
⊢ (𝑅:𝑄⟶(0[,]+∞) → dom 𝑅 = 𝑄) |
16 | 15 | 3ad2ant2 1125 |
. . . . 5
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ dom 𝑅 = 𝑄) |
17 | 16 | unieqd 4683 |
. . . 4
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ ∪ dom 𝑅 = ∪ 𝑄) |
18 | 14, 17 | sseqtr4d 3861 |
. . 3
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ 𝐴 ⊆ ∪ dom 𝑅) |
19 | | elex 3414 |
. . . . . 6
⊢ (𝑄 ∈ 𝑉 → 𝑄 ∈ V) |
20 | | uniexb 7252 |
. . . . . . 7
⊢ (𝑄 ∈ V ↔ ∪ 𝑄
∈ V) |
21 | 20 | biimpi 208 |
. . . . . 6
⊢ (𝑄 ∈ V → ∪ 𝑄
∈ V) |
22 | 2, 19, 21 | 3syl 18 |
. . . . 5
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ ∪ 𝑄 ∈ V) |
23 | | ssexg 5043 |
. . . . 5
⊢ ((𝐴 ⊆ ∪ 𝑄
∧ ∪ 𝑄 ∈ V) → 𝐴 ∈ V) |
24 | 14, 22, 23 | syl2anc 579 |
. . . 4
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ 𝐴 ∈
V) |
25 | | elpwg 4387 |
. . . 4
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
26 | 24, 25 | syl 17 |
. . 3
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ (𝐴 ∈ 𝒫
∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
27 | 18, 26 | mpbird 249 |
. 2
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ 𝐴 ∈ 𝒫
∪ dom 𝑅) |
28 | | xrltso 12288 |
. . . 4
⊢ < Or
ℝ* |
29 | | iccssxr 12572 |
. . . . 5
⊢
(0[,]+∞) ⊆ ℝ* |
30 | | soss 5295 |
. . . . 5
⊢
((0[,]+∞) ⊆ ℝ* → ( < Or
ℝ* → < Or (0[,]+∞))) |
31 | 29, 30 | ax-mp 5 |
. . . 4
⊢ ( < Or
ℝ* → < Or (0[,]+∞)) |
32 | 28, 31 | mp1i 13 |
. . 3
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ < Or (0[,]+∞)) |
33 | 32 | infexd 8679 |
. 2
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ inf(ran (𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < ) ∈
V) |
34 | 6, 13, 27, 33 | fvmptd 6550 |
1
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑅‘𝑦)), (0[,]+∞), < )) |