Theorem ovn0val

Description: The Lebesgue outer measure (for the zero dimensional space of reals) of every subset is zero. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypothesis	ovn0val.1	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m ∅ ) )
Assertion	ovn0val	⊢ ( 𝜑 → ( ( voln* ‘ ∅ ) ‘ 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ovn0val.1	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m ∅ ) )
2		0fin	⊢ ∅ ∈ Fin
3	2	a1i	⊢ ( 𝜑 → ∅ ∈ Fin )
4		eqid	⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m ∅ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ ∅ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ ∅ ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m ∅ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ ∅ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ ∅ ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
5	3 1 4	ovnval2	⊢ ( 𝜑 → ( ( voln* ‘ ∅ ) ‘ 𝐴 ) = if ( ∅ = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m ∅ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ ∅ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ ∅ ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) )
6		eqid	⊢ ∅ = ∅
7		iftrue	⊢ ( ∅ = ∅ → if ( ∅ = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m ∅ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ ∅ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ ∅ ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) = 0 )
8	6 7	ax-mp	⊢ if ( ∅ = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m ∅ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ ∅ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ ∅ ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) = 0
9	8	a1i	⊢ ( 𝜑 → if ( ∅ = ∅ , 0 , inf ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m ∅ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ ∅ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ ∅ ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } , ℝ* , < ) ) = 0 )
10	5 9	eqtrd	⊢ ( 𝜑 → ( ( voln* ‘ ∅ ) ‘ 𝐴 ) = 0 )