ovnsslelem

Description: The (multidimensional, nonzero-dimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnsslelem.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovnsslelem.2	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	ovnsslelem.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	ovnsslelem.4	⊢ ( 𝜑 → 𝐵 ⊆ ( ℝ ↑_m 𝑋 ) )
	ovnsslelem.5	⊢ 𝑀 = { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
	ovnsslelem.6	⊢ 𝑁 = { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
Assertion	ovnsslelem	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ovnsslelem.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovnsslelem.2	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3		ovnsslelem.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
4		ovnsslelem.4	⊢ ( 𝜑 → 𝐵 ⊆ ( ℝ ↑_m 𝑋 ) )
5		ovnsslelem.5	⊢ 𝑀 = { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
6		ovnsslelem.6	⊢ 𝑁 = { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → 𝐴 ⊆ 𝐵 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
9	7 8	sstrd	⊢ ( ( 𝜑 ∧ 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
10	9	adantrr	⊢ ( ( 𝜑 ∧ ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) )
11		simprr	⊢ ( ( 𝜑 ∧ ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
12	10 11	jca	⊢ ( ( 𝜑 ∧ ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) )
13	12	ex	⊢ ( 𝜑 → ( ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
14	13	reximdv	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ^* ) → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) )
16	15	ss2rabdv	⊢ ( 𝜑 → { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ { 𝑧 ∈ ℝ^* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑_m 𝑋 ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^{^} ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
17	16 6 5	3sstr4g	⊢ ( 𝜑 → 𝑁 ⊆ 𝑀 )
18	5	ssrab3	⊢ 𝑀 ⊆ ℝ^*
19		infxrss	⊢ ( ( 𝑁 ⊆ 𝑀 ∧ 𝑀 ⊆ ℝ^* ) → inf ( 𝑀 , ℝ^* , < ) ≤ inf ( 𝑁 , ℝ^* , < ) )
20	17 18 19	sylancl	⊢ ( 𝜑 → inf ( 𝑀 , ℝ^* , < ) ≤ inf ( 𝑁 , ℝ^* , < ) )
21	3 4	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑_m 𝑋 ) )
22	1 2 21 5	ovnn0val	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )
23	1 2 4 6	ovnn0val	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) = inf ( 𝑁 , ℝ^* , < ) )
24	20 22 23	3brtr4d	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) )

Metamath Proof Explorer

Theorem ovnsslelem

Proof