Step | Hyp | Ref
| Expression |
1 | | ovolval4lem2.a |
. 2
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
2 | | ovolval4lem2.m |
. . 3
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} |
3 | | iftrue 4445 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))) = (2nd ‘(𝑓‘𝑛))) |
4 | 3 | opeq2d 4791 |
. . . . . . . . . . . . . 14
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → 〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉 = 〈(1st
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛))〉) |
5 | 4 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 =
〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉) |
6 | | df-br 5054 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) ↔ 〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉 ∈ ≤ ) |
7 | 6 | biimpi 219 |
. . . . . . . . . . . . . 14
⊢
((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → 〈(1st ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛))〉 ∈ ≤ ) |
8 | 7 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛))〉 ∈ ≤
) |
9 | 5, 8 | eqeltrd 2838 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ≤
) |
10 | | iffalse 4448 |
. . . . . . . . . . . . . . 15
⊢ (¬
(1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))) = (1st ‘(𝑓‘𝑛))) |
11 | 10 | opeq2d 4791 |
. . . . . . . . . . . . . 14
⊢ (¬
(1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)) → 〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉 = 〈(1st
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))〉) |
12 | 11 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ ¬ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 =
〈(1st ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))〉) |
13 | | elmapi 8530 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝑓:ℕ⟶(ℝ ×
ℝ)) |
14 | 13 | ffvelrnda 6904 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ (ℝ ×
ℝ)) |
15 | | xp1st 7793 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑛) ∈ (ℝ × ℝ) →
(1st ‘(𝑓‘𝑛)) ∈ ℝ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝑓‘𝑛)) ∈
ℝ) |
17 | 16 | leidd 11398 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝑓‘𝑛)) ≤ (1st
‘(𝑓‘𝑛))) |
18 | | df-br 5054 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝑓‘𝑛)) ≤ (1st ‘(𝑓‘𝑛)) ↔ 〈(1st ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛))〉 ∈ ≤ ) |
19 | 17, 18 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))〉 ∈ ≤
) |
20 | 19 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ ¬ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))〉 ∈ ≤
) |
21 | 12, 20 | eqeltrd 2838 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ ¬ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ≤
) |
22 | 9, 21 | pm2.61dan 813 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ≤
) |
23 | | xp2nd 7794 |
. . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑛) ∈ (ℝ × ℝ) →
(2nd ‘(𝑓‘𝑛)) ∈ ℝ) |
24 | 14, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝑓‘𝑛)) ∈
ℝ) |
25 | 24, 16 | ifcld 4485 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))) ∈
ℝ) |
26 | | opelxpi 5588 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝑓‘𝑛)) ∈ ℝ ∧ if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛))) ∈ ℝ) →
〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉 ∈ (ℝ ×
ℝ)) |
27 | 16, 25, 26 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ (ℝ
× ℝ)) |
28 | 22, 27 | elind 4108 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉 ∈ ( ≤ ∩
(ℝ × ℝ))) |
29 | | ovolval4lem2.g |
. . . . . . . . . 10
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st
‘(𝑓‘𝑛)), if((1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛)), (2nd
‘(𝑓‘𝑛)), (1st
‘(𝑓‘𝑛)))〉) |
30 | 28, 29 | fmptd 6931 |
. . . . . . . . 9
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
31 | | reex 10820 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
32 | 31, 31 | xpex 7538 |
. . . . . . . . . . . 12
⊢ (ℝ
× ℝ) ∈ V |
33 | 32 | inex2 5211 |
. . . . . . . . . . 11
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ( ≤ ∩ (ℝ ×
ℝ)) ∈ V) |
35 | | nnex 11836 |
. . . . . . . . . . 11
⊢ ℕ
∈ V |
36 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ℕ ∈ V) |
37 | 34, 36 | elmapd 8522 |
. . . . . . . . 9
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ)))) |
38 | 30, 37 | mpbird 260 |
. . . . . . . 8
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) |
39 | 38 | adantr 484 |
. . . . . . 7
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝐺 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) |
40 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝑓)) |
41 | | rexpssxrxp 10878 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (ℝ × ℝ) ⊆
(ℝ* × ℝ*)) |
43 | 13, 42 | fssd 6563 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝑓:ℕ⟶(ℝ* ×
ℝ*)) |
44 | | 2fveq3 6722 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (1st ‘(𝑓‘𝑘)) = (1st ‘(𝑓‘𝑛))) |
45 | | 2fveq3 6722 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (2nd ‘(𝑓‘𝑘)) = (2nd ‘(𝑓‘𝑛))) |
46 | 44, 45 | breq12d 5066 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((1st ‘(𝑓‘𝑘)) ≤ (2nd ‘(𝑓‘𝑘)) ↔ (1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)))) |
47 | 46 | cbvrabv 3402 |
. . . . . . . . . . . . 13
⊢ {𝑘 ∈ ℕ ∣
(1st ‘(𝑓‘𝑘)) ≤ (2nd ‘(𝑓‘𝑘))} = {𝑛 ∈ ℕ ∣ (1st
‘(𝑓‘𝑛)) ≤ (2nd
‘(𝑓‘𝑛))} |
48 | 43, 29, 47 | ovolval4lem1 43862 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (∪ ran
((,) ∘ 𝑓) = ∪ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝑓)) = (vol ∘ ((,) ∘
𝐺)))) |
49 | 48 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ∪ ran
((,) ∘ 𝑓) = ∪ ran ((,) ∘ 𝐺)) |
50 | 49 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
∪ ran ((,) ∘ 𝑓) = ∪ ran ((,)
∘ 𝐺)) |
51 | 40, 50 | sseqtrd 3941 |
. . . . . . . . 9
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝑓)) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝐺)) |
52 | 51 | adantrr 717 |
. . . . . . . 8
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐺)) |
53 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) |
54 | 48 | simprd 499 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → (vol ∘ ((,) ∘ 𝑓)) = (vol ∘ ((,) ∘
𝐺))) |
55 | | coass 6129 |
. . . . . . . . . . . . . 14
⊢ ((vol
∘ (,)) ∘ 𝑓) =
(vol ∘ ((,) ∘ 𝑓)) |
56 | 55 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((vol ∘ (,)) ∘ 𝑓) = (vol ∘ ((,) ∘
𝑓))) |
57 | | coass 6129 |
. . . . . . . . . . . . . 14
⊢ ((vol
∘ (,)) ∘ 𝐺) =
(vol ∘ ((,) ∘ 𝐺)) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((vol ∘ (,)) ∘ 𝐺) = (vol ∘ ((,) ∘
𝐺))) |
59 | 54, 56, 58 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ (,)) ∘
𝐺)) |
60 | 59 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) |
61 | 60 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) |
62 | 53, 61 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) |
63 | 62 | adantrl 716 |
. . . . . . . 8
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) |
64 | 52, 63 | jca 515 |
. . . . . . 7
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺)))) |
65 | | coeq2 5727 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → ((,) ∘ 𝑔) = ((,) ∘ 𝐺)) |
66 | 65 | rneqd 5807 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ran ((,) ∘ 𝑔) = ran ((,) ∘ 𝐺)) |
67 | 66 | unieqd 4833 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ∪ ran
((,) ∘ 𝑔) = ∪ ran ((,) ∘ 𝐺)) |
68 | 67 | sseq2d 3933 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ↔
𝐴 ⊆ ∪ ran ((,) ∘ 𝐺))) |
69 | | coeq2 5727 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((vol ∘ (,)) ∘ 𝑔) = ((vol ∘ (,)) ∘
𝐺)) |
70 | 69 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 →
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))) |
71 | 70 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)) ↔ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺)))) |
72 | 68, 71 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺))))) |
73 | 72 | rspcev 3537 |
. . . . . . 7
⊢ ((𝐺 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝐺)))) → ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
74 | 39, 64, 73 | syl2anc 587 |
. . . . . 6
⊢ ((𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) → ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
75 | 74 | rexlimiva 3200 |
. . . . 5
⊢
(∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) → ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
76 | | inss2 4144 |
. . . . . . . . . 10
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
77 | | mapss 8570 |
. . . . . . . . . 10
⊢
(((ℝ × ℝ) ∈ V ∧ ( ≤ ∩ (ℝ ×
ℝ)) ⊆ (ℝ × ℝ)) → (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ⊆ ((ℝ ×
ℝ) ↑m ℕ)) |
78 | 32, 76, 77 | mp2an 692 |
. . . . . . . . 9
⊢ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ) ⊆ ((ℝ
× ℝ) ↑m ℕ) |
79 | 78 | sseli 3896 |
. . . . . . . 8
⊢ (𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) → 𝑔 ∈ ((ℝ × ℝ)
↑m ℕ)) |
80 | 79 | adantr 484 |
. . . . . . 7
⊢ ((𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → 𝑔 ∈ ((ℝ × ℝ)
↑m ℕ)) |
81 | | simpr 488 |
. . . . . . 7
⊢ ((𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
82 | | coeq2 5727 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → ((,) ∘ 𝑓) = ((,) ∘ 𝑔)) |
83 | 82 | rneqd 5807 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ran ((,) ∘ 𝑓) = ran ((,) ∘ 𝑔)) |
84 | 83 | unieqd 4833 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ∪ ran ((,)
∘ 𝑓) = ∪ ran ((,) ∘ 𝑔)) |
85 | 84 | sseq2d 3933 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ↔
𝐴 ⊆ ∪ ran ((,) ∘ 𝑔))) |
86 | | coeq2 5727 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((vol ∘ (,)) ∘ 𝑓) = ((vol ∘ (,)) ∘
𝑔)) |
87 | 86 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 →
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) |
88 | 87 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)) ↔ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
89 | 85, 88 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))))) |
90 | 89 | rspcev 3537 |
. . . . . . 7
⊢ ((𝑔 ∈ ((ℝ ×
ℝ) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
91 | 80, 81, 90 | syl2anc 587 |
. . . . . 6
⊢ ((𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
92 | 91 | rexlimiva 3200 |
. . . . 5
⊢
(∃𝑔 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔))) → ∃𝑓 ∈ ((ℝ ×
ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))) |
93 | 75, 92 | impbii 212 |
. . . 4
⊢
(∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓))) ↔ ∃𝑔 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))) |
94 | 93 | rabbii 3383 |
. . 3
⊢ {𝑦 ∈ ℝ*
∣ ∃𝑓 ∈
((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑓)))} = {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} |
95 | 2, 94 | eqtri 2765 |
. 2
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑔 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑔) ∧ 𝑦 =
(Σ^‘((vol ∘ (,)) ∘ 𝑔)))} |
96 | 1, 95 | ovolval3 43860 |
1
⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, <
)) |