Theorem ovnovol

Description: The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnovol.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ovnovol.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
Assertion	ovnovol	⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = ( vol* ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ovnovol.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		ovnovol.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
3		eqid	⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m { 𝐴 } ) ↑m ℕ ) ( ( 𝐵 ↑m { 𝐴 } ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ { 𝐴 } ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ { 𝐴 } ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
4		eqeq1	⊢ ( 𝑤 = 𝑧 → ( 𝑤 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ↔ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) )
5	4	anbi2d	⊢ ( 𝑤 = 𝑧 → ( ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑤 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
6	5	rexbidv	⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑤 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) ) )
7	6	cbvrabv	⊢ { 𝑤 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑤 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
8	1 2 3 7	ovnovollem3	⊢ ( 𝜑 → ( ( voln* ‘ { 𝐴 } ) ‘ ( 𝐵 ↑m { 𝐴 } ) ) = ( vol* ‘ 𝐵 ) )