Metamath Proof Explorer

Theorem ovolval4

Description: The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 , but here f may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Hypotheses	ovolval4.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
		ovolval4.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
	Assertion	ovolval4	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ovolval4.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ovolval4.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^{^} ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
3		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) )
4		2fveq3	⊢ ( 𝑘 = 𝑛 → ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
5	3 4	breq12d	⊢ ( 𝑘 = 𝑛 → ( ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) ↔ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
6	5 4 3	ifbieq12d	⊢ ( 𝑘 = 𝑛 → if ( ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ) = if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
7	3 6	opeq12d	⊢ ( 𝑘 = 𝑛 → ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ )
8	7	cbvmptv	⊢ ( 𝑘 ∈ ℕ ↦ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑘 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑘 ) ) ) ⟩ ) = ( 𝑛 ∈ ℕ ↦ ⟨ ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) , if ( ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝑓 ‘ 𝑛 ) ) , ( 1^st ‘ ( 𝑓 ‘ 𝑛 ) ) ) ⟩ )
9	1 2 8	ovolval4lem2	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )