Proof of Theorem ovnval2b
Step | Hyp | Ref
| Expression |
1 | | ovnval2b.1 |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | ovnval2b.2 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) |
3 | | eqid 2737 |
. . 3
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
4 | 1, 2, 3 | ovnval2 43758 |
. 2
⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
))) |
5 | | biidd 265 |
. . 3
⊢ (𝜑 → (𝑋 = ∅ ↔ 𝑋 = ∅)) |
6 | | ovnval2b.3 |
. . . . . 6
⊢ 𝐿 = (𝑎 ∈ 𝒫 (ℝ ↑m
𝑋) ↦ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
7 | | cleq1lem 14545 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → ((𝑎 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
8 | 7 | rexbidv 3216 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝑎 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
9 | 8 | rabbidv 3390 |
. . . . . 6
⊢ (𝑎 = 𝐴 → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
10 | | ovexd 7248 |
. . . . . . . 8
⊢ (𝜑 → (ℝ
↑m 𝑋)
∈ V) |
11 | 10, 2 | ssexd 5217 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ V) |
12 | 11, 2 | elpwd 4521 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝒫 (ℝ
↑m 𝑋)) |
13 | | xrex 12583 |
. . . . . . . 8
⊢
ℝ* ∈ V |
14 | 13 | rabex 5225 |
. . . . . . 7
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∈ V |
15 | 14 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∈ V) |
16 | 6, 9, 12, 15 | fvmptd3 6841 |
. . . . 5
⊢ (𝜑 → (𝐿‘𝐴) = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
17 | 16 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = (𝐿‘𝐴)) |
18 | 17 | infeq1d 9093 |
. . 3
⊢ (𝜑 → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) =
inf((𝐿‘𝐴), ℝ*, <
)) |
19 | 5, 18 | ifbieq2d 4465 |
. 2
⊢ (𝜑 → if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )) =
if(𝑋 = ∅, 0,
inf((𝐿‘𝐴), ℝ*, <
))) |
20 | 4, 19 | eqtrd 2777 |
1
⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = if(𝑋 = ∅, 0, inf((𝐿‘𝐴), ℝ*, <
))) |