Theorem ovnssle

Description: The (multidimensional) 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	ovnssle.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovnssle.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	ovnssle.3	⊢ ( 𝜑 → 𝐵 ⊆ ( ℝ ↑m 𝑋 ) )
Assertion	ovnssle	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ovnssle.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovnssle.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
3		ovnssle.3	⊢ ( 𝜑 → 𝐵 ⊆ ( ℝ ↑m 𝑋 ) )
4		0le0	⊢ 0 ≤ 0
5	4	a1i	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 0 ≤ 0 )
6		fveq2	⊢ ( 𝑋 = ∅ → ( voln* ‘ 𝑋 ) = ( voln* ‘ ∅ ) )
7	6	fveq1d	⊢ ( 𝑋 = ∅ → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ ∅ ) ‘ 𝐴 ) )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ ∅ ) ‘ 𝐴 ) )
9	2	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 ⊆ 𝐵 )
10	3	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐵 ⊆ ( ℝ ↑m 𝑋 ) )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝑋 = ∅ )
12	11	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ℝ ↑m 𝑋 ) = ( ℝ ↑m ∅ ) )
13	10 12	sseqtrd	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐵 ⊆ ( ℝ ↑m ∅ ) )
14	9 13	sstrd	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝐴 ⊆ ( ℝ ↑m ∅ ) )
15	14	ovn0val	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ ∅ ) ‘ 𝐴 ) = 0 )
16	8 15	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = 0 )
17	6	fveq1d	⊢ ( 𝑋 = ∅ → ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) = ( ( voln* ‘ ∅ ) ‘ 𝐵 ) )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) = ( ( voln* ‘ ∅ ) ‘ 𝐵 ) )
19	13	ovn0val	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ ∅ ) ‘ 𝐵 ) = 0 )
20	18 19	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) = 0 )
21	16 20	breq12d	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) ↔ 0 ≤ 0 ) )
22	5 21	mpbird	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) )
23	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ∈ Fin )
24		neqne	⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
25	24	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
26	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝐴 ⊆ 𝐵 )
27	3	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝐵 ⊆ ( ℝ ↑m 𝑋 ) )
28		eqid	⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
29		eqid	⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐵 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
30	23 25 26 27 28 29	ovnsslelem	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) )
31	22 30	pm2.61dan	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝐵 ) )