Step |
Hyp |
Ref |
Expression |
1 |
|
ovnf.1 |
⊢ ( 𝜑 → 𝑋 ∈ Fin ) |
2 |
|
0e0iccpnf |
⊢ 0 ∈ ( 0 [,] +∞ ) |
3 |
2
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → 0 ∈ ( 0 [,] +∞ ) ) |
4 |
|
0xr |
⊢ 0 ∈ ℝ* |
5 |
4
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → 0 ∈ ℝ* ) |
6 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
7 |
6
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → +∞ ∈ ℝ* ) |
8 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → 𝑋 ∈ Fin ) |
9 |
|
elpwi |
⊢ ( 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) → 𝑦 ⊆ ( ℝ ↑m 𝑋 ) ) |
10 |
9
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → 𝑦 ⊆ ( ℝ ↑m 𝑋 ) ) |
11 |
|
eqid |
⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } |
12 |
8 10 11
|
ovnsupge0 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ( 0 [,] +∞ ) ) |
13 |
8 10 11
|
ovnpnfelsup |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → +∞ ∈ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ) |
14 |
13
|
ne0d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ≠ ∅ ) |
15 |
5 7 12 14
|
inficc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ∈ ( 0 [,] +∞ ) ) |
16 |
3 15
|
ifcld |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) → if ( 𝑋 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) ∈ ( 0 [,] +∞ ) ) |
17 |
|
eqid |
⊢ ( 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ if ( 𝑋 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) ) = ( 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ if ( 𝑋 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) ) |
18 |
16 17
|
fmptd |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ if ( 𝑋 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) ) : 𝒫 ( ℝ ↑m 𝑋 ) ⟶ ( 0 [,] +∞ ) ) |
19 |
1
|
ovnval |
⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) = ( 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ if ( 𝑋 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) ) ) |
20 |
19
|
feq1d |
⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) : 𝒫 ( ℝ ↑m 𝑋 ) ⟶ ( 0 [,] +∞ ) ↔ ( 𝑦 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ if ( 𝑋 = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) ) : 𝒫 ( ℝ ↑m 𝑋 ) ⟶ ( 0 [,] +∞ ) ) ) |
21 |
18 20
|
mpbird |
⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) : 𝒫 ( ℝ ↑m 𝑋 ) ⟶ ( 0 [,] +∞ ) ) |