Theorem ovolval5

Description: The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		ovolval5.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ovolval5.m	⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( [,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ [,) ) ∘ 𝑓 ) ) ) }
3		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ↔ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) )
4	3	anbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) )
5	4	rexbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ) )
6		coeq2	⊢ ( 𝑔 = 𝑓 → ( (,) ∘ 𝑔 ) = ( (,) ∘ 𝑓 ) )
7	6	rneqd	⊢ ( 𝑔 = 𝑓 → ran ( (,) ∘ 𝑔 ) = ran ( (,) ∘ 𝑓 ) )
8	7	unieqd	⊢ ( 𝑔 = 𝑓 → ∪ ran ( (,) ∘ 𝑔 ) = ∪ ran ( (,) ∘ 𝑓 ) )
9	8	sseq2d	⊢ ( 𝑔 = 𝑓 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) )
10		coeq2	⊢ ( 𝑔 = 𝑓 → ( ( vol ∘ (,) ) ∘ 𝑔 ) = ( ( vol ∘ (,) ) ∘ 𝑓 ) )
11	10	fveq2d	⊢ ( 𝑔 = 𝑓 → ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) )
12	11	eqeq2d	⊢ ( 𝑔 = 𝑓 → ( 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ↔ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
13	9 12	anbi12d	⊢ ( 𝑔 = 𝑓 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
14	13	cbvrexvw	⊢ ( ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
15	14	a1i	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
16	5 15	bitrd	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
17	16	cbvrabv	⊢ { 𝑥 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
18	1 17	ovolval4	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( { 𝑥 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) } , ℝ* , < ) )
19	11	eqeq2d	⊢ ( 𝑔 = 𝑓 → ( 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ↔ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
20	9 19	anbi12d	⊢ ( 𝑔 = 𝑓 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
21	20	cbvrexvw	⊢ ( ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
22	21	a1i	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
23		eqeq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ↔ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) )
24	23	anbi2d	⊢ ( 𝑥 = 𝑧 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
25	24	rexbidv	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
26	22 25	bitrd	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) ↔ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) ) )
27	26	cbvrabv	⊢ { 𝑥 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑓 ) ) ) }
28	2 27	ovolval5lem3	⊢ inf ( { 𝑥 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) } , ℝ* , < ) = inf ( 𝑀 , ℝ* , < )
29	28	a1i	⊢ ( 𝜑 → inf ( { 𝑥 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ℝ × ℝ ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = ( Σ^ ‘ ( ( vol ∘ (,) ) ∘ 𝑔 ) ) ) } , ℝ* , < ) = inf ( 𝑀 , ℝ* , < ) )
30	18 29	eqtrd	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ* , < ) )