Step | Hyp | Ref
| Expression |
1 | | ovolval4lem2.a |
. 2
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
2 | | ovolval4lem2.m |
. . 3
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
3 | | iftrue 4042 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))) = (2nd ‘(𝑓‘𝑛))) |
4 | 3 | opeq2d 4347 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → 〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉 = 〈(1st
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛))〉) |
5 | 4 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 =
〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉) |
6 | | df-br 4584 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) ↔ 〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉 ∈ ≤ ) |
7 | 6 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → 〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉 ∈ ≤ ) |
8 | 7 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛))〉 ∈ ≤
) |
9 | 5, 8 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ≤
) |
10 | | iffalse 4045 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))) = (1st ‘(𝑓‘𝑛))) |
11 | 10 | opeq2d 4347 |
. . . . . . . . . . . . . . 15
⊢ (¬
(1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → 〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉 = 〈(1st
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))〉) |
12 | 11 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) ∧ ¬ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 =
〈(1st ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))〉) |
13 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
14 | 13 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ (ℝ ×
ℝ)) |
15 | | xp1st 7089 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓‘𝑛) ∈ (ℝ × ℝ) →
(1st ‘(𝑓‘𝑛)) ∈ ℝ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝑓‘𝑛)) ∈
ℝ) |
17 | 16 | leidd 10473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝑓‘𝑛)) ≤ (1st
‘(𝑓‘𝑛))) |
18 | | df-br 4584 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝑓‘𝑛)) ≤ (1st ‘(𝑓‘𝑛)) ↔ 〈(1st ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))〉 ∈ ≤ ) |
19 | 17, 18 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))〉 ∈ ≤
) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) ∧ ¬ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))〉 ∈ ≤
) |
21 | 12, 20 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) ∧ ¬ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ≤
) |
22 | 9, 21 | pm2.61dan 828 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ≤
) |
23 | | xp2nd 7090 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑛) ∈ (ℝ × ℝ) →
(2nd ‘(𝑓‘𝑛)) ∈ ℝ) |
24 | 14, 23 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝑓‘𝑛)) ∈
ℝ) |
25 | 24, 16 | ifcld 4081 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))) ∈
ℝ) |
26 | | opelxpi 5072 |
. . . . . . . . . . . . 13
⊢
(((1st ‘(𝑓‘𝑛)) ∈ ℝ ∧ if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))) ∈ ℝ) →
〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉 ∈ (ℝ ×
ℝ)) |
27 | 16, 25, 26 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ (ℝ
× ℝ)) |
28 | 22, 27 | elind 3760 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ( ≤ ∩
(ℝ × ℝ))) |
29 | | ovolval4lem2.g |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉) |
30 | 28, 29 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
31 | | reex 9906 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
32 | 31, 31 | xpex 6860 |
. . . . . . . . . . . . 13
⊢ (ℝ
× ℝ) ∈ V |
33 | 32 | inex2 4728 |
. . . . . . . . . . . 12
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ( ≤ ∩ (ℝ
× ℝ)) ∈ V) |
35 | | nnex 10903 |
. . . . . . . . . . . 12
⊢ ℕ
∈ V |
36 | 35 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ℕ ∈
V) |
37 | 34, 36 | elmapd 7758 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → (𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ)))) |
38 | 30, 37 | mpbird 246 |
. . . . . . . . 9
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → 𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
39 | 38 | adantr 480 |
. . . . . . . 8
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
40 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓)) |
41 | | rexpssxrxp 9963 |
. . . . . . . . . . . . . . . 16
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → (ℝ × ℝ)
⊆ (ℝ* × ℝ*)) |
43 | 13, 42 | fssd 5970 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → 𝑓:ℕ⟶(ℝ* ×
ℝ*)) |
44 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑓‘𝑘) = (𝑓‘𝑛)) |
45 | 44 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (1st ‘(𝑓‘𝑘)) = (1st ‘(𝑓‘𝑛))) |
46 | 44 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (2nd ‘(𝑓‘𝑘)) = (2nd ‘(𝑓‘𝑛))) |
47 | 45, 46 | breq12d 4596 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → ((1st ‘(𝑓‘𝑘)) ≤ (2nd ‘(𝑓‘𝑘)) ↔ (1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)))) |
48 | 47 | cbvrabv 3172 |
. . . . . . . . . . . . . 14
⊢ {𝑘 ∈ ℕ ∣
(1st ‘(𝑓‘𝑘)) ≤ (2nd ‘(𝑓‘𝑘))} = {𝑛 ∈ ℕ ∣ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))} |
49 | 43, 29, 48 | ovolval4lem1 39539 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → (∪ ran ((,) ∘ 𝑓) = ∪ ran ((,)
∘ 𝐺) ∧ (vol
∘ ((,) ∘ 𝑓)) =
(vol ∘ ((,) ∘ 𝐺)))) |
50 | 49 | simpld 474 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ∪ ran ((,) ∘ 𝑓) = ∪ ran ((,)
∘ 𝐺)) |
51 | 50 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
∪ ran ((,) ∘ 𝑓) = ∪ ran ((,)
∘ 𝐺)) |
52 | 40, 51 | sseqtrd 3604 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝐺)) |
53 | 52 | adantrr 749 |
. . . . . . . . 9
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐺)) |
54 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) |
55 | 49 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → (vol ∘ ((,) ∘
𝑓)) = (vol ∘ ((,)
∘ 𝐺))) |
56 | | coass 5571 |
. . . . . . . . . . . . . . 15
⊢ ((vol
∘ (,)) ∘ 𝑓) =
(vol ∘ ((,) ∘ 𝑓)) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ((vol ∘ (,)) ∘
𝑓) = (vol ∘ ((,)
∘ 𝑓))) |
58 | | coass 5571 |
. . . . . . . . . . . . . . 15
⊢ ((vol
∘ (,)) ∘ 𝐺) =
(vol ∘ ((,) ∘ 𝐺)) |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ((vol ∘ (,)) ∘
𝐺) = (vol ∘ ((,)
∘ 𝐺))) |
60 | 55, 57, 59 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → ((vol ∘ (,)) ∘
𝑓) = ((vol ∘ (,))
∘ 𝐺)) |
61 | 60 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) |
62 | 61 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) |
63 | 54, 62 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) |
64 | 63 | adantrl 748 |
. . . . . . . . 9
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) |
65 | 53, 64 | jca 553 |
. . . . . . . 8
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺)))) |
66 | | coeq2 5202 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → ((,) ∘ 𝑔) = ((,) ∘ 𝐺)) |
67 | 66 | rneqd 5274 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → ran ((,) ∘ 𝑔) = ran ((,) ∘ 𝐺)) |
68 | 67 | unieqd 4382 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ∪ ran
((,) ∘ 𝑔) = ∪ ran ((,) ∘ 𝐺)) |
69 | 68 | sseq2d 3596 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ↔
𝐴 ⊆ ∪ ran ((,) ∘ 𝐺))) |
70 | | coeq2 5202 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → ((vol ∘ (,)) ∘ 𝑔) = ((vol ∘ (,)) ∘
𝐺)) |
71 | 70 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 →
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) |
72 | 71 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) ↔ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺)))) |
73 | 69, 72 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))))) |
74 | 73 | rspcev 3282 |
. . . . . . . 8
⊢ ((𝐺 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺)))) → ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
75 | 39, 65, 74 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
76 | 75 | rexlimiva 3010 |
. . . . . 6
⊢
(∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
77 | | inss2 3796 |
. . . . . . . . . . 11
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
78 | | mapss 7786 |
. . . . . . . . . . 11
⊢
(((ℝ × ℝ) ∈ V ∧ ( ≤ ∩ (ℝ ×
ℝ)) ⊆ (ℝ × ℝ)) → (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ⊆ ((ℝ ×
ℝ) ↑𝑚 ℕ)) |
79 | 32, 77, 78 | mp2an 704 |
. . . . . . . . . 10
⊢ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ) ⊆
((ℝ × ℝ) ↑𝑚 ℕ) |
80 | 79 | sseli 3564 |
. . . . . . . . 9
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → 𝑔 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) |
81 | 80 | adantr 480 |
. . . . . . . 8
⊢ ((𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → 𝑔 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) |
82 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
83 | | coeq2 5202 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → ((,) ∘ 𝑓) = ((,) ∘ 𝑔)) |
84 | 83 | rneqd 5274 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝑔)) |
85 | 84 | unieqd 4382 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ∪ ran ((,)
∘ 𝑓) = ∪ ran ((,) ∘ 𝑔)) |
86 | 85 | sseq2d 3596 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ↔
𝐴 ⊆ ∪ ran ((,) ∘ 𝑔))) |
87 | | coeq2 5202 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ (,)) ∘
𝑔)) |
88 | 87 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) |
89 | 88 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
90 | 86, 89 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))))) |
91 | 90 | rspcev 3282 |
. . . . . . . 8
⊢ ((𝑔 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
92 | 81, 82, 91 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
93 | 92 | rexlimiva 3010 |
. . . . . 6
⊢
(∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
94 | 76, 93 | impbii 198 |
. . . . 5
⊢
(∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
95 | 94 | a1i 11 |
. . . 4
⊢ (𝑦 ∈ ℝ*
→ (∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))))) |
96 | 95 | rabbiia 3161 |
. . 3
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} = {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} |
97 | 2, 96 | eqtri 2632 |
. 2
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} |
98 | 1, 97 | ovolval3 39537 |
1
⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, <
)) |