This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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* ‘ 𝐵 ) )