Metamath Proof Explorer


Theorem ovnf

Description: The Lebesgue outer measure is a function that maps sets to nonnegative extended reals. This is step (a)(i) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis ovnf.1 ( 𝜑𝑋 ∈ Fin )
Assertion ovnf ( 𝜑 → ( voln* ‘ 𝑋 ) : 𝒫 ( ℝ ↑m 𝑋 ) ⟶ ( 0 [,] +∞ ) )

Proof

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 [,] +∞ ) )