Theorem ovnlerp

Description: The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnlerp.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovnlerp.n0	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	ovnlerp.a	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
	ovnlerp.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	ovnlerp.m	⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
Assertion	ovnlerp	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑀 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		ovnlerp.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovnlerp.n0	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3		ovnlerp.a	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
4		ovnlerp.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
5		ovnlerp.m	⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
6		nfv	⊢ Ⅎ 𝑥 𝜑
7		ssrab2	⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ℝ*
8	5 7	eqsstri	⊢ 𝑀 ⊆ ℝ*
9	8	a1i	⊢ ( 𝜑 → 𝑀 ⊆ ℝ* )
10	1 3 5	ovnpnfelsup	⊢ ( 𝜑 → +∞ ∈ 𝑀 )
11	10	ne0d	⊢ ( 𝜑 → 𝑀 ≠ ∅ )
12		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
13	1 3 5	ovnsupge0	⊢ ( 𝜑 → 𝑀 ⊆ ( 0 [,] +∞ ) )
14		0xr	⊢ 0 ∈ ℝ*
15	14	a1i	⊢ ( ( 𝑀 ⊆ ( 0 [,] +∞ ) ∧ 𝑦 ∈ 𝑀 ) → 0 ∈ ℝ* )
16		pnfxr	⊢ +∞ ∈ ℝ*
17	16	a1i	⊢ ( ( 𝑀 ⊆ ( 0 [,] +∞ ) ∧ 𝑦 ∈ 𝑀 ) → +∞ ∈ ℝ* )
18		ssel2	⊢ ( ( 𝑀 ⊆ ( 0 [,] +∞ ) ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ( 0 [,] +∞ ) )
19		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝑦 )
20	15 17 18 19	syl3anc	⊢ ( ( 𝑀 ⊆ ( 0 [,] +∞ ) ∧ 𝑦 ∈ 𝑀 ) → 0 ≤ 𝑦 )
21	20	ralrimiva	⊢ ( 𝑀 ⊆ ( 0 [,] +∞ ) → ∀ 𝑦 ∈ 𝑀 0 ≤ 𝑦 )
22	13 21	syl	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑀 0 ≤ 𝑦 )
23		breq1	⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑦 ↔ 0 ≤ 𝑦 ) )
24	23	ralbidv	⊢ ( 𝑥 = 0 → ( ∀ 𝑦 ∈ 𝑀 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑀 0 ≤ 𝑦 ) )
25	24	rspcev	⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑀 0 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑀 𝑥 ≤ 𝑦 )
26	12 22 25	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑀 𝑥 ≤ 𝑦 )
27	6 9 11 26 4	infrpge	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑀 𝑤 ≤ ( inf ( 𝑀 , ℝ* , < ) +e 𝐸 ) )
28		nfv	⊢ Ⅎ 𝑤 𝜑
29		simp3	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑀 ∧ 𝑤 ≤ ( inf ( 𝑀 , ℝ* , < ) +e 𝐸 ) ) → 𝑤 ≤ ( inf ( 𝑀 , ℝ* , < ) +e 𝐸 ) )
30	1 2 3 5	ovnn0val	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = inf ( 𝑀 , ℝ* , < ) )
31	30	eqcomd	⊢ ( 𝜑 → inf ( 𝑀 , ℝ* , < ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) )
32	31	oveq1d	⊢ ( 𝜑 → ( inf ( 𝑀 , ℝ* , < ) +e 𝐸 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
33	32	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑀 ∧ 𝑤 ≤ ( inf ( 𝑀 , ℝ* , < ) +e 𝐸 ) ) → ( inf ( 𝑀 , ℝ* , < ) +e 𝐸 ) = ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
34	29 33	breqtrd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑀 ∧ 𝑤 ≤ ( inf ( 𝑀 , ℝ* , < ) +e 𝐸 ) ) → 𝑤 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
35	34	3exp	⊢ ( 𝜑 → ( 𝑤 ∈ 𝑀 → ( 𝑤 ≤ ( inf ( 𝑀 , ℝ* , < ) +e 𝐸 ) → 𝑤 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) ) )
36	28 35	reximdai	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ 𝑀 𝑤 ≤ ( inf ( 𝑀 , ℝ* , < ) +e 𝐸 ) → ∃ 𝑤 ∈ 𝑀 𝑤 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) )
37	27 36	mpd	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑀 𝑤 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
38		nfcv	⊢ Ⅎ 𝑤 𝑀
39		nfrab1	⊢ Ⅎ 𝑧 { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
40	5 39	nfcxfr	⊢ Ⅎ 𝑧 𝑀
41		nfv	⊢ Ⅎ 𝑧 𝑤 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 )
42		nfv	⊢ Ⅎ 𝑤 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 )
43		breq1	⊢ ( 𝑤 = 𝑧 → ( 𝑤 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ↔ 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ) )
44	38 40 41 42 43	cbvrexfw	⊢ ( ∃ 𝑤 ∈ 𝑀 𝑤 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) ↔ ∃ 𝑧 ∈ 𝑀 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )
45	37 44	sylib	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑀 𝑧 ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) +e 𝐸 ) )