| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-ovoln 46552 | . 2
⊢ voln* =
(𝑥 ∈ Fin ↦
(𝑦 ∈ 𝒫
(ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
)))) | 
| 2 |  | oveq2 7439 | . . . 4
⊢ (𝑥 = 𝑋 → (ℝ ↑m 𝑥) = (ℝ ↑m
𝑋)) | 
| 3 | 2 | pweqd 4617 | . . 3
⊢ (𝑥 = 𝑋 → 𝒫 (ℝ
↑m 𝑥) =
𝒫 (ℝ ↑m 𝑋)) | 
| 4 |  | eqeq1 2741 | . . . 4
⊢ (𝑥 = 𝑋 → (𝑥 = ∅ ↔ 𝑋 = ∅)) | 
| 5 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → ((ℝ × ℝ)
↑m 𝑥) =
((ℝ × ℝ) ↑m 𝑋)) | 
| 6 | 5 | oveq1d 7446 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (((ℝ × ℝ)
↑m 𝑥)
↑m ℕ) = (((ℝ × ℝ) ↑m
𝑋) ↑m
ℕ)) | 
| 7 |  | ixpeq1 8948 | . . . . . . . . . 10
⊢ (𝑥 = 𝑋 → X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) | 
| 8 | 7 | iuneq2d 5022 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) | 
| 9 | 8 | sseq2d 4016 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ 𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) | 
| 10 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑥 = 𝑋 ∧ 𝑗 ∈ ℕ) → 𝑥 = 𝑋) | 
| 11 | 10 | prodeq1d 15956 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑋 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) | 
| 12 | 11 | mpteq2dva 5242 | . . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) | 
| 13 | 12 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) | 
| 14 | 13 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) | 
| 15 | 9, 14 | anbi12d 632 | . . . . . . 7
⊢ (𝑥 = 𝑋 → ((𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) | 
| 16 | 6, 15 | rexeqbidv 3347 | . . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑥)
↑m ℕ)(𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) | 
| 17 | 16 | rabbidv 3444 | . . . . 5
⊢ (𝑥 = 𝑋 → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) | 
| 18 | 17 | infeq1d 9517 | . . . 4
⊢ (𝑥 = 𝑋 → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) =
inf({𝑧 ∈
ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
)) | 
| 19 | 4, 18 | ifbieq2d 4552 | . . 3
⊢ (𝑥 = 𝑋 → if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )) =
if(𝑋 = ∅, 0,
inf({𝑧 ∈
ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
))) | 
| 20 | 3, 19 | mpteq12dv 5233 | . 2
⊢ (𝑥 = 𝑋 → (𝑦 ∈ 𝒫 (ℝ ↑m
𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ))) =
(𝑦 ∈ 𝒫
(ℝ ↑m 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
)))) | 
| 21 |  | ovnval.1 | . 2
⊢ (𝜑 → 𝑋 ∈ Fin) | 
| 22 |  | ovex 7464 | . . . . 5
⊢ (ℝ
↑m 𝑋)
∈ V | 
| 23 | 22 | pwex 5380 | . . . 4
⊢ 𝒫
(ℝ ↑m 𝑋) ∈ V | 
| 24 | 23 | mptex 7243 | . . 3
⊢ (𝑦 ∈ 𝒫 (ℝ
↑m 𝑋)
↦ if(𝑋 = ∅, 0,
inf({𝑧 ∈
ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ))) ∈
V | 
| 25 | 24 | a1i 11 | . 2
⊢ (𝜑 → (𝑦 ∈ 𝒫 (ℝ ↑m
𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ))) ∈
V) | 
| 26 | 1, 20, 21, 25 | fvmptd3 7039 | 1
⊢ (𝜑 → (voln*‘𝑋) = (𝑦 ∈ 𝒫 (ℝ ↑m
𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
)))) |