Theorem ovolss

Description: The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014)

	Ref	Expression
Assertion	ovolss	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
2		eqid	⊢ { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
3	1 2	ovolsslem	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ 𝐵 ) )