Step | Hyp | Ref
| Expression |
1 | | sstr2 3575 |
. . . . . . . . 9
⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝑓) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓))) |
2 | 1 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) ∧ 𝑦 ∈ ℝ*) → (𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) → 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓))) |
3 | 2 | anim1d 586 |
. . . . . . 7
⊢ (((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) ∧ 𝑦 ∈ ℝ*) → ((𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, <
)))) |
4 | 3 | reximdv 2999 |
. . . . . 6
⊢ (((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) ∧ 𝑦 ∈ ℝ*) →
(∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, <
)))) |
5 | 4 | ss2rabdv 3646 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))}) |
6 | | ovolss.2 |
. . . . 5
⊢ 𝑁 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} |
7 | | ovolss.1 |
. . . . 5
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} |
8 | 5, 6, 7 | 3sstr4g 3609 |
. . . 4
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → 𝑁 ⊆ 𝑀) |
9 | | sstr 3576 |
. . . . 5
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → 𝐴 ⊆ ℝ) |
10 | 7 | ovolval 23049 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ →
(vol*‘𝐴) = inf(𝑀, ℝ*, <
)) |
11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝑀) → (vol*‘𝐴) = inf(𝑀, ℝ*, <
)) |
12 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} ⊆ ℝ* |
13 | 7, 12 | eqsstri 3598 |
. . . . . . . . 9
⊢ 𝑀 ⊆
ℝ* |
14 | | infxrlb 12036 |
. . . . . . . . 9
⊢ ((𝑀 ⊆ ℝ*
∧ 𝑥 ∈ 𝑀) → inf(𝑀, ℝ*, < ) ≤ 𝑥) |
15 | 13, 14 | mpan 702 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑀 → inf(𝑀, ℝ*, < ) ≤ 𝑥) |
16 | 15 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝑀) → inf(𝑀, ℝ*, < ) ≤ 𝑥) |
17 | 11, 16 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝑀) → (vol*‘𝐴) ≤ 𝑥) |
18 | 17 | ralrimiva 2949 |
. . . . 5
⊢ (𝐴 ⊆ ℝ →
∀𝑥 ∈ 𝑀 (vol*‘𝐴) ≤ 𝑥) |
19 | 9, 18 | syl 17 |
. . . 4
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → ∀𝑥 ∈ 𝑀 (vol*‘𝐴) ≤ 𝑥) |
20 | | ssralv 3629 |
. . . 4
⊢ (𝑁 ⊆ 𝑀 → (∀𝑥 ∈ 𝑀 (vol*‘𝐴) ≤ 𝑥 → ∀𝑥 ∈ 𝑁 (vol*‘𝐴) ≤ 𝑥)) |
21 | 8, 19, 20 | sylc 63 |
. . 3
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → ∀𝑥 ∈ 𝑁 (vol*‘𝐴) ≤ 𝑥) |
22 | | ssrab2 3650 |
. . . . 5
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} ⊆ ℝ* |
23 | 6, 22 | eqsstri 3598 |
. . . 4
⊢ 𝑁 ⊆
ℝ* |
24 | | ovolcl 23053 |
. . . . 5
⊢ (𝐴 ⊆ ℝ →
(vol*‘𝐴) ∈
ℝ*) |
25 | 9, 24 | syl 17 |
. . . 4
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ∈
ℝ*) |
26 | | infxrgelb 12037 |
. . . 4
⊢ ((𝑁 ⊆ ℝ*
∧ (vol*‘𝐴) ∈
ℝ*) → ((vol*‘𝐴) ≤ inf(𝑁, ℝ*, < ) ↔
∀𝑥 ∈ 𝑁 (vol*‘𝐴) ≤ 𝑥)) |
27 | 23, 25, 26 | sylancr 694 |
. . 3
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → ((vol*‘𝐴) ≤ inf(𝑁, ℝ*, < ) ↔
∀𝑥 ∈ 𝑁 (vol*‘𝐴) ≤ 𝑥)) |
28 | 21, 27 | mpbird 246 |
. 2
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ inf(𝑁, ℝ*, <
)) |
29 | 6 | ovolval 23049 |
. . 3
⊢ (𝐵 ⊆ ℝ →
(vol*‘𝐵) = inf(𝑁, ℝ*, <
)) |
30 | 29 | adantl 481 |
. 2
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐵) = inf(𝑁, ℝ*, <
)) |
31 | 28, 30 | breqtrrd 4611 |
1
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵)) |