ovolsslem

Description: Lemma for ovolss . (Contributed by Mario Carneiro, 16-Mar-2014) (Proof shortened by AV, 17-Sep-2020)

	Ref	Expression
Hypotheses	ovolss.1	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) }
	ovolss.2	⊢ 𝑁 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) }
Assertion	ovolsslem	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ovolss.1	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) }
2		ovolss.2	⊢ 𝑁 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) }
3		sstr2	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) )
4	3	ad2antrr	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) ∧ 𝑦 ∈ ℝ^* ) → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) )
5	4	anim1d	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) ∧ 𝑦 ∈ ℝ^* ) → ( ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) ) )
6	5	reximdv	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) ∧ 𝑦 ∈ ℝ^* ) → ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) ) )
7	6	ss2rabdv	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } ⊆ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } )
8	7 2 1	3sstr4g	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → 𝑁 ⊆ 𝑀 )
9		sstr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → 𝐴 ⊆ ℝ )
10	1	ovolval	⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )
11	10	adantr	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝑀 ) → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ^* , < ) )
12	1	ssrab3	⊢ 𝑀 ⊆ ℝ^*
13		infxrlb	⊢ ( ( 𝑀 ⊆ ℝ^* ∧ 𝑥 ∈ 𝑀 ) → inf ( 𝑀 , ℝ^* , < ) ≤ 𝑥 )
14	12 13	mpan	⊢ ( 𝑥 ∈ 𝑀 → inf ( 𝑀 , ℝ^* , < ) ≤ 𝑥 )
15	14	adantl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝑀 ) → inf ( 𝑀 , ℝ^* , < ) ≤ 𝑥 )
16	11 15	eqbrtrd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝑀 ) → ( vol* ‘ 𝐴 ) ≤ 𝑥 )
17	16	ralrimiva	⊢ ( 𝐴 ⊆ ℝ → ∀ 𝑥 ∈ 𝑀 ( vol* ‘ 𝐴 ) ≤ 𝑥 )
18	9 17	syl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ∀ 𝑥 ∈ 𝑀 ( vol* ‘ 𝐴 ) ≤ 𝑥 )
19		ssralv	⊢ ( 𝑁 ⊆ 𝑀 → ( ∀ 𝑥 ∈ 𝑀 ( vol* ‘ 𝐴 ) ≤ 𝑥 → ∀ 𝑥 ∈ 𝑁 ( vol* ‘ 𝐴 ) ≤ 𝑥 ) )
20	8 18 19	sylc	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ∀ 𝑥 ∈ 𝑁 ( vol* ‘ 𝐴 ) ≤ 𝑥 )
21	2	ssrab3	⊢ 𝑁 ⊆ ℝ^*
22		ovolcl	⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) ∈ ℝ^* )
23	9 22	syl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ( vol* ‘ 𝐴 ) ∈ ℝ^* )
24		infxrgelb	⊢ ( ( 𝑁 ⊆ ℝ^* ∧ ( vol* ‘ 𝐴 ) ∈ ℝ^* ) → ( ( vol* ‘ 𝐴 ) ≤ inf ( 𝑁 , ℝ^* , < ) ↔ ∀ 𝑥 ∈ 𝑁 ( vol* ‘ 𝐴 ) ≤ 𝑥 ) )
25	21 23 24	sylancr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ( ( vol* ‘ 𝐴 ) ≤ inf ( 𝑁 , ℝ^* , < ) ↔ ∀ 𝑥 ∈ 𝑁 ( vol* ‘ 𝐴 ) ≤ 𝑥 ) )
26	20 25	mpbird	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ( vol* ‘ 𝐴 ) ≤ inf ( 𝑁 , ℝ^* , < ) )
27	2	ovolval	⊢ ( 𝐵 ⊆ ℝ → ( vol* ‘ 𝐵 ) = inf ( 𝑁 , ℝ^* , < ) )
28	27	adantl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ( vol* ‘ 𝐵 ) = inf ( 𝑁 , ℝ^* , < ) )
29	26 28	breqtrrd	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ 𝐵 ) )

Metamath Proof Explorer

Theorem ovolsslem

Proof