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