Step | Hyp | Ref
| Expression |
1 | | ovolval5lem3.q |
. . . . 5
⊢ 𝑄 = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
2 | | ssrab2 3993 |
. . . . 5
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆
ℝ* |
3 | 1, 2 | eqsstri 3935 |
. . . 4
⊢ 𝑄 ⊆
ℝ* |
4 | | infxrcl 12923 |
. . . 4
⊢ (𝑄 ⊆ ℝ*
→ inf(𝑄,
ℝ*, < ) ∈ ℝ*) |
5 | 3, 4 | mp1i 13 |
. . 3
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) ∈ ℝ*) |
6 | | ovolval5lem3.m |
. . . . 5
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} |
7 | | ssrab2 3993 |
. . . . 5
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} ⊆
ℝ* |
8 | 6, 7 | eqsstri 3935 |
. . . 4
⊢ 𝑀 ⊆
ℝ* |
9 | | infxrcl 12923 |
. . . 4
⊢ (𝑀 ⊆ ℝ*
→ inf(𝑀,
ℝ*, < ) ∈ ℝ*) |
10 | 8, 9 | mp1i 13 |
. . 3
⊢ (⊤
→ inf(𝑀,
ℝ*, < ) ∈ ℝ*) |
11 | 3 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝑄 ⊆
ℝ*) |
12 | 8 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝑀 ⊆
ℝ*) |
13 | | simpr 488 |
. . . . . 6
⊢ ((𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) |
14 | 6 | rabeq2i 3398 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ ℝ* ∧
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
15 | 14 | biimpi 219 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑀 → (𝑦 ∈ ℝ* ∧
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
16 | 15 | simprd 499 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑀 → ∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
17 | 16 | adantr 484 |
. . . . . 6
⊢ ((𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+) →
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
18 | | coeq2 5727 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = 𝑓 → ((,) ∘ 𝑔) = ((,) ∘ 𝑓)) |
19 | 18 | rneqd 5807 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑓 → ran ((,) ∘ 𝑔) = ran ((,) ∘ 𝑓)) |
20 | 19 | unieqd 4833 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑓 → ∪ ran ((,)
∘ 𝑔) = ∪ ran ((,) ∘ 𝑓)) |
21 | 20 | sseq2d 3933 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ↔
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓))) |
22 | | coeq2 5727 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑓 → ((vol ∘ (,)) ∘ 𝑔) = ((vol ∘ (,)) ∘
𝑓)) |
23 | 22 | fveq2d 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑓 →
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) |
24 | 23 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → (𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) ↔ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
25 | 21, 24 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑓 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) |
26 | 25 | cbvrexvw 3359 |
. . . . . . . . . . . 12
⊢
(∃𝑔 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
27 | 26 | rabbii 3383 |
. . . . . . . . . . 11
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑔 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
28 | 1, 27 | eqtr4i 2768 |
. . . . . . . . . 10
⊢ 𝑄 = {𝑧 ∈ ℝ* ∣
∃𝑔 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} |
29 | | simp3r 1204 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
30 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Σ^‘((vol ∘ (,)) ∘
(𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉))) =
(Σ^‘((vol ∘ (,)) ∘ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉))) |
31 | | elmapi 8530 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
32 | 31 | 3ad2ant2 1136 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
33 | | simp3l 1203 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐴 ⊆ ∪ ran
([,) ∘ 𝑓)) |
34 | | simp1 1138 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑤 ∈ ℝ+) |
35 | | 2fveq3 6722 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (1st ‘(𝑓‘𝑚)) = (1st ‘(𝑓‘𝑛))) |
36 | | oveq2 7221 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛)) |
37 | 36 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑤 / (2↑𝑚)) = (𝑤 / (2↑𝑛))) |
38 | 35, 37 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))) = ((1st ‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛)))) |
39 | | 2fveq3 6722 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (2nd ‘(𝑓‘𝑚)) = (2nd ‘(𝑓‘𝑛))) |
40 | 38, 39 | opeq12d 4792 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → 〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉 = 〈((1st
‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛))), (2nd ‘(𝑓‘𝑛))〉) |
41 | 40 | cbvmptv 5158 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑚)) − (𝑤 / (2↑𝑚))), (2nd ‘(𝑓‘𝑚))〉) = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝑓‘𝑛)) − (𝑤 / (2↑𝑛))), (2nd ‘(𝑓‘𝑛))〉) |
42 | 28, 29, 30, 32, 33, 34, 41 | ovolval5lem2 43866 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ+
∧ 𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
43 | 42 | 3exp 1121 |
. . . . . . . 8
⊢ (𝑤 ∈ ℝ+
→ (𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ) → ((𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)))) |
44 | 43 | rexlimdv 3202 |
. . . . . . 7
⊢ (𝑤 ∈ ℝ+
→ (∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤))) |
45 | 44 | imp 410 |
. . . . . 6
⊢ ((𝑤 ∈ ℝ+
∧ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
46 | 13, 17, 45 | syl2anc 587 |
. . . . 5
⊢ ((𝑦 ∈ 𝑀 ∧ 𝑤 ∈ ℝ+) →
∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
47 | 46 | 3adant1 1132 |
. . . 4
⊢
((⊤ ∧ 𝑦
∈ 𝑀 ∧ 𝑤 ∈ ℝ+)
→ ∃𝑧 ∈
𝑄 𝑧 ≤ (𝑦 +𝑒 𝑤)) |
48 | 11, 12, 47 | infleinf 42584 |
. . 3
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) ≤ inf(𝑀, ℝ*, <
)) |
49 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
50 | 49 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) |
51 | 50 | rexbidv 3216 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))))) |
52 | 51 | cbvrabv 3402 |
. . . . . . 7
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
53 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓)) |
54 | | ioossico 13026 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛))) ⊆ ((1st ‘(𝑓‘𝑛))[,)(2nd ‘(𝑓‘𝑛))) |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝑓‘𝑛))(,)(2nd
‘(𝑓‘𝑛))) ⊆ ((1st
‘(𝑓‘𝑛))[,)(2nd
‘(𝑓‘𝑛)))) |
56 | 31 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
57 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
58 | 56, 57 | fvovco 42405 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝑓)‘𝑛) = ((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛)))) |
59 | 56, 57 | fvovco 42405 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (([,) ∘ 𝑓)‘𝑛) = ((1st ‘(𝑓‘𝑛))[,)(2nd ‘(𝑓‘𝑛)))) |
60 | 58, 59 | sseq12d 3934 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛) ↔ ((1st ‘(𝑓‘𝑛))(,)(2nd ‘(𝑓‘𝑛))) ⊆ ((1st ‘(𝑓‘𝑛))[,)(2nd ‘(𝑓‘𝑛))))) |
61 | 55, 60 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛)) |
62 | 61 | ralrimiva 3105 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∀𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛)) |
63 | | ss2iun 4922 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑛 ∈
ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ (([,) ∘ 𝑓)‘𝑛) → ∪
𝑛 ∈ ℕ (((,)
∘ 𝑓)‘𝑛) ⊆ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛)) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪
𝑛 ∈ ℕ (((,)
∘ 𝑓)‘𝑛) ⊆ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛)) |
65 | | ioof 13035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (,):(ℝ* ×
ℝ*)⟶𝒫 ℝ) |
67 | | rexpssxrxp 10878 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (ℝ × ℝ) ⊆
(ℝ* × ℝ*)) |
69 | 31, 68 | fssd 6563 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝑓:ℕ⟶(ℝ* ×
ℝ*)) |
70 | | fco 6569 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((,):(ℝ* × ℝ*)⟶𝒫
ℝ ∧ 𝑓:ℕ⟶(ℝ* ×
ℝ*)) → ((,) ∘ 𝑓):ℕ⟶𝒫
ℝ) |
71 | 66, 69, 70 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((,) ∘ 𝑓):ℕ⟶𝒫
ℝ) |
72 | 71 | ffnd 6546 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((,) ∘ 𝑓) Fn ℕ) |
73 | | fniunfv 7060 |
. . . . . . . . . . . . . . . . . 18
⊢ (((,)
∘ 𝑓) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) = ∪ ran ((,)
∘ 𝑓)) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪
𝑛 ∈ ℕ (((,)
∘ 𝑓)‘𝑛) = ∪
ran ((,) ∘ 𝑓)) |
75 | | icof 42432 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
[,):(ℝ* × ℝ*)⟶𝒫
ℝ* |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → [,):(ℝ* ×
ℝ*)⟶𝒫 ℝ*) |
77 | | fco 6569 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(([,):(ℝ* × ℝ*)⟶𝒫
ℝ* ∧ 𝑓:ℕ⟶(ℝ* ×
ℝ*)) → ([,) ∘ 𝑓):ℕ⟶𝒫
ℝ*) |
78 | 76, 69, 77 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ([,) ∘ 𝑓):ℕ⟶𝒫
ℝ*) |
79 | 78 | ffnd 6546 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ([,) ∘ 𝑓) Fn ℕ) |
80 | | fniunfv 7060 |
. . . . . . . . . . . . . . . . . 18
⊢ (([,)
∘ 𝑓) Fn ℕ
→ ∪ 𝑛 ∈ ℕ (([,) ∘ 𝑓)‘𝑛) = ∪ ran ([,)
∘ 𝑓)) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪
𝑛 ∈ ℕ (([,)
∘ 𝑓)‘𝑛) = ∪
ran ([,) ∘ 𝑓)) |
82 | 74, 81 | sseq12d 3934 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (∪ 𝑛 ∈ ℕ (((,) ∘ 𝑓)‘𝑛) ⊆ ∪
𝑛 ∈ ℕ (([,)
∘ 𝑓)‘𝑛) ↔ ∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran
([,) ∘ 𝑓))) |
83 | 64, 82 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪ ran
((,) ∘ 𝑓) ⊆
∪ ran ([,) ∘ 𝑓)) |
84 | 83 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
∪ ran ((,) ∘ 𝑓) ⊆ ∪ ran
([,) ∘ 𝑓)) |
85 | 53, 84 | sstrd 3911 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ([,) ∘ 𝑓)) |
86 | 85 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝐴 ⊆ ∪ ran
([,) ∘ 𝑓)) |
87 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) |
88 | 31 | voliooicof 43212 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ [,)) ∘
𝑓)) |
89 | 88 | fveq2d 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
90 | 89 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
91 | 87, 90 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
92 | 91 | adantrl 716 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
93 | 86, 92 | jca 515 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
94 | 93 | ex 416 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → (𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
95 | 94 | reximia 3165 |
. . . . . . . . 9
⊢
(∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
96 | 95 | rgenw 3073 |
. . . . . . . 8
⊢
∀𝑦 ∈
ℝ* (∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
97 | | ss2rab 3984 |
. . . . . . . 8
⊢ ({𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} ↔ ∀𝑦 ∈ ℝ*
(∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
98 | 96, 97 | mpbir 234 |
. . . . . . 7
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} |
99 | 52, 98 | eqsstri 3935 |
. . . . . 6
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} |
100 | 1, 6 | sseq12i 3931 |
. . . . . 6
⊢ (𝑄 ⊆ 𝑀 ↔ {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⊆ {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))}) |
101 | 99, 100 | mpbir 234 |
. . . . 5
⊢ 𝑄 ⊆ 𝑀 |
102 | | infxrss 12929 |
. . . . 5
⊢ ((𝑄 ⊆ 𝑀 ∧ 𝑀 ⊆ ℝ*) →
inf(𝑀, ℝ*,
< ) ≤ inf(𝑄,
ℝ*, < )) |
103 | 101, 8, 102 | mp2an 692 |
. . . 4
⊢ inf(𝑀, ℝ*, < )
≤ inf(𝑄,
ℝ*, < ) |
104 | 103 | a1i 11 |
. . 3
⊢ (⊤
→ inf(𝑀,
ℝ*, < ) ≤ inf(𝑄, ℝ*, <
)) |
105 | 5, 10, 48, 104 | xrletrid 12745 |
. 2
⊢ (⊤
→ inf(𝑄,
ℝ*, < ) = inf(𝑀, ℝ*, <
)) |
106 | 105 | mptru 1550 |
1
⊢ inf(𝑄, ℝ*, < ) =
inf(𝑀, ℝ*,
< ) |