Step | Hyp | Ref
| Expression |
1 | | ovolval5lem3.q |
. . . . 5
⊢ 𝑄 = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
2 | 1 | ssrab3 4040 |
. . . 4
⊢ 𝑄 ⊆
ℝ* |
3 | | infxrcl 13252 |
. . . 4
⊢ (𝑄 ⊆ ℝ*
→ inf(𝑄,
ℝ*, < ) ∈ ℝ*) |
4 | 2, 3 | mp1i 13 |
. . 3
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) ∈ ℝ*) |
5 | | ovolval5lem3.m |
. . . . 5
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} |
6 | 5 | ssrab3 4040 |
. . . 4
⊢ 𝑀 ⊆
ℝ* |
7 | | infxrcl 13252 |
. . . 4
⊢ (𝑀 ⊆ ℝ*
→ inf(𝑀,
ℝ*, < ) ∈ ℝ*) |
8 | 6, 7 | mp1i 13 |
. . 3
⊢ (⊤
→ inf(𝑀,
ℝ*, < ) ∈ ℝ*) |
9 | 2 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝑄 ⊆
ℝ*) |
10 | 6 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝑀 ⊆
ℝ*) |
11 | 5 | reqabi 3429 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ ℝ* ∧
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
12 | 11 | simprbi 497 |
. . . . . 6
⊢ (𝑦 ∈ 𝑀 → ∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
13 | | coeq2 5814 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑓 → ((,) ∘ 𝑔) = ((,) ∘ 𝑓)) |
14 | 13 | rneqd 5893 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → ran ((,) ∘ 𝑔) = ran ((,) ∘ 𝑓)) |
15 | 14 | unieqd 4879 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑓 → ∪ ran ((,)
∘ 𝑔) = ∪ ran ((,) ∘ 𝑓)) |
16 | 15 | sseq2d 3976 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑓 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ↔
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓))) |
17 | | coeq2 5814 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → ((vol ∘ (,)) ∘ 𝑔) = ((vol ∘ (,)) ∘
𝑓)) |
18 | 17 | fveq2d 6846 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑓 →
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) |
19 | 18 | eqeq2d 2747 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑓 → (𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) ↔ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
20 | 16, 19 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑓 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) |
21 | 20 | cbvrexvw 3226 |
. . . . . . . . . 10
⊢
(∃𝑔 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
22 | 21 | rabbii 3413 |
. . . . . . . . 9
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑔 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
23 | 1, 22 | eqtr4i 2767 |
. . . . . . . 8
⊢ 𝑄 = {𝑧 ∈ ℝ* ∣
∃𝑔 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} |
24 | | simp3r 1202 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
25 | | eqid 2736 |
. . . . . . . 8
⊢
(Σ^‘((vol ∘ (,)) ∘
(𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉))) =
(Σ^‘((vol ∘ (,)) ∘ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉))) |
26 | | elmapi 8787 |
. . . . . . . . 9
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
27 | 26 | 3ad2ant2 1134 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
28 | | simp3l 1201 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐴 ⊆ ∪ ran
([,) ∘ 𝑓)) |
29 | | simp1 1136 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑤 ∈ ℝ+) |
30 | | 2fveq3 6847 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (1st ‘(𝑓‘𝑚)) = (1st ‘(𝑓‘𝑛))) |
31 | | oveq2 7365 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛)) |
32 | 31 | oveq2d 7373 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑤 / (2↑𝑚)) = (𝑤 / (2↑𝑛))) |
33 | 30, 32 | oveq12d 7375 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))) = ((1st ‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛)))) |
34 | | 2fveq3 6847 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (2nd ‘(𝑓‘𝑚)) = (2nd ‘(𝑓‘𝑛))) |
35 | 33, 34 | opeq12d 4838 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → 〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉 = 〈((1st
‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛))), (2nd ‘(𝑓‘𝑛))〉) |
36 | 35 | cbvmptv 5218 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉) = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛))), (2nd ‘(𝑓‘𝑛))〉) |
37 | 23, 24, 25, 27, 28, 29, 36 | ovolval5lem2 44884 |
. . . . . . 7
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
38 | 37 | rexlimdv3a 3156 |
. . . . . 6
⊢ (𝑤 ∈ ℝ+
→ (∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤))) |
39 | 12, 38 | mpan9 507 |
. . . . 5
⊢ ((𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+) →
∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
40 | 39 | 3adant1 1130 |
. . . 4
⊢
((⊤ ∧ 𝑦
∈ 𝑀 ∧ 𝑤 ∈ ℝ+)
→ ∃𝑧 ∈
𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
41 | 9, 10, 40 | infleinf 43596 |
. . 3
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) ≤ inf(𝑀, ℝ*, <
)) |
42 | | eqeq1 2740 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
43 | 42 | anbi2d 629 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) |
44 | 43 | rexbidv 3175 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) |
45 | 44 | cbvrabv 3417 |
. . . . . . 7
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
46 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓)) |
47 | | ioossico 13355 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛))) ⊆ ((1st ‘(𝑓‘𝑛))[,)(2nd ‘(𝑓‘𝑛))) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝑓‘𝑛))(,)(2nd
‘(𝑓‘𝑛))) ⊆ ((1st
‘(𝑓‘𝑛))[,)(2nd
‘(𝑓‘𝑛)))) |
49 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
50 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
51 | 49, 50 | fvovco 43403 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝑓)‘𝑛) = ((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛)))) |
52 | 49, 50 | fvovco 43403 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (([,) ∘ 𝑓)‘𝑛) = ((1st ‘(𝑓‘𝑛))[,)(2nd ‘(𝑓‘𝑛)))) |
53 | 48, 51, 52 | 3sstr4d 3991 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛)) |
54 | 53 | ralrimiva 3143 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∀𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛)) |
55 | | ss2iun 4972 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛) → ∪
𝑛 ∈ ℕ (((,)
∘ 𝑓)‘𝑛) ⊆ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪
𝑛 ∈ ℕ (((,)
∘ 𝑓)‘𝑛) ⊆ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛)) |
57 | | ioof 13364 |
. . . . . . . . . . . . . . . . . . 19
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (,):(ℝ* ×
ℝ*)⟶𝒫 ℝ) |
59 | | rexpssxrxp 11200 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (ℝ × ℝ) ⊆
(ℝ* × ℝ*)) |
61 | 58, 60, 26 | fcoss 43421 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((,) ∘ 𝑓):ℕ⟶𝒫
ℝ) |
62 | 61 | ffnd 6669 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((,) ∘ 𝑓) Fn ℕ) |
63 | | fniunfv 7194 |
. . . . . . . . . . . . . . . 16
⊢ (((,)
∘ 𝑓) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) = ∪ ran ((,)
∘ 𝑓)) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪
𝑛 ∈ ℕ (((,)
∘ 𝑓)‘𝑛) = ∪
ran ((,) ∘ 𝑓)) |
65 | | icof 43430 |
. . . . . . . . . . . . . . . . . . 19
⊢
[,):(ℝ* × ℝ*)⟶𝒫
ℝ* |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → [,):(ℝ* ×
ℝ*)⟶𝒫 ℝ*) |
67 | 66, 60, 26 | fcoss 43421 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ([,) ∘ 𝑓):ℕ⟶𝒫
ℝ*) |
68 | 67 | ffnd 6669 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ([,) ∘ 𝑓) Fn ℕ) |
69 | | fniunfv 7194 |
. . . . . . . . . . . . . . . 16
⊢ (([,)
∘ 𝑓) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛) = ∪ ran ([,)
∘ 𝑓)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪
𝑛 ∈ ℕ (([,)
∘ 𝑓)‘𝑛) = ∪
ran ([,) ∘ 𝑓)) |
71 | 56, 64, 70 | 3sstr3d 3990 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪ ran
((,) ∘ 𝑓) ⊆
∪ ran ([,) ∘ 𝑓)) |
72 | 71 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran
([,) ∘ 𝑓)) |
73 | 46, 72 | sstrd 3954 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ([,) ∘ 𝑓)) |
74 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) |
75 | 26 | voliooicof 44227 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ [,)) ∘
𝑓)) |
76 | 75 | fveq2d 6846 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
77 | 76 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
78 | 74, 77 | eqtrd 2776 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
79 | 73, 78 | anim12dan 619 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
80 | 79 | ex 413 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
81 | 80 | reximia 3084 |
. . . . . . . . 9
⊢
(∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
82 | 81 | a1i 11 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ*
→ (∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
83 | 82 | ss2rabi 4034 |
. . . . . . 7
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} |
84 | 45, 83 | eqsstri 3978 |
. . . . . 6
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} |
85 | 84, 1, 5 | 3sstr4i 3987 |
. . . . 5
⊢ 𝑄 ⊆ 𝑀 |
86 | | infxrss 13258 |
. . . . 5
⊢ ((𝑄 ⊆ 𝑀 ∧ 𝑀 ⊆ ℝ*) →
inf(𝑀, ℝ*,
< ) ≤ inf(𝑄,
ℝ*, < )) |
87 | 85, 6, 86 | mp2an 690 |
. . . 4
⊢ inf(𝑀, ℝ*, < )
≤ inf(𝑄,
ℝ*, < ) |
88 | 87 | a1i 11 |
. . 3
⊢ (⊤
→ inf(𝑀,
ℝ*, < ) ≤ inf(𝑄, ℝ*, <
)) |
89 | 4, 8, 41, 88 | xrletrid 13074 |
. 2
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) = inf(𝑀, ℝ*, <
)) |
90 | 89 | mptru 1548 |
1
⊢ inf(𝑄, ℝ*, < ) =
inf(𝑀, ℝ*,
< ) |