Step |
Hyp |
Ref |
Expression |
1 |
|
uniioombl.1 |
⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
2 |
|
uniioombl.2 |
⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) ) |
3 |
|
uniioombl.3 |
⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) |
4 |
|
uniioombl.a |
⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 ) |
5 |
|
uniioombl.e |
⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ ) |
6 |
|
uniioombl.c |
⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) |
7 |
|
uniioombl.g |
⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
8 |
|
uniioombl.s |
⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ) |
9 |
|
uniioombl.t |
⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) |
10 |
|
uniioombl.v |
⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) ) |
11 |
|
uniioombl.m |
⊢ ( 𝜑 → 𝑀 ∈ ℕ ) |
12 |
|
uniioombl.m2 |
⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 ) |
13 |
|
uniioombl.k |
⊢ 𝐾 = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) |
14 |
|
ioof |
⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ |
15 |
|
inss2 |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) |
16 |
|
rexpssxrxp |
⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* ) |
17 |
15 16
|
sstri |
⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) |
18 |
|
fss |
⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) ) |
19 |
7 17 18
|
sylancl |
⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) ) |
20 |
|
fco |
⊢ ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ ) |
21 |
14 19 20
|
sylancr |
⊢ ( 𝜑 → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ ) |
22 |
|
ffun |
⊢ ( ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ → Fun ( (,) ∘ 𝐺 ) ) |
23 |
|
funiunfv |
⊢ ( Fun ( (,) ∘ 𝐺 ) → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ) |
24 |
21 22 23
|
3syl |
⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ) |
25 |
|
elfznn |
⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℕ ) |
26 |
|
fvco3 |
⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) |
27 |
7 25 26
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) |
28 |
27
|
iuneq2dv |
⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑗 ) = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) |
29 |
24 28
|
eqtr3d |
⊢ ( 𝜑 → ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) |
30 |
13 29
|
syl5eq |
⊢ ( 𝜑 → 𝐾 = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) |
31 |
|
ffvelrn |
⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
32 |
7 25 31
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) ) |
33 |
32
|
elin2d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) ) |
34 |
|
1st2nd2 |
⊢ ( ( 𝐺 ‘ 𝑗 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝑗 ) = 〈 ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) 〉 ) |
35 |
33 34
|
syl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑗 ) = 〈 ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) 〉 ) |
36 |
35
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( (,) ‘ 〈 ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) 〉 ) ) |
37 |
|
df-ov |
⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( (,) ‘ 〈 ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) , ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) 〉 ) |
38 |
36 37
|
eqtr4di |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) = ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) |
39 |
|
ioossre |
⊢ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ⊆ ℝ |
40 |
38 39
|
eqsstrdi |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ) |
41 |
40
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ) |
42 |
|
iunss |
⊢ ( ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ↔ ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ) |
43 |
41 42
|
sylibr |
⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ) |
44 |
30 43
|
eqsstrd |
⊢ ( 𝜑 → 𝐾 ⊆ ℝ ) |
45 |
|
fzfid |
⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin ) |
46 |
38
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) ) |
47 |
|
ovolfcl |
⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) |
48 |
7 25 47
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) |
49 |
|
ovolioo |
⊢ ( ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) |
50 |
48 49
|
syl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) (,) ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) |
51 |
46 50
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) |
52 |
48
|
simp2d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ) |
53 |
48
|
simp1d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ ) |
54 |
52 53
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( 2nd ‘ ( 𝐺 ‘ 𝑗 ) ) − ( 1st ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) |
55 |
51 54
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) |
56 |
45 55
|
fsumrecl |
⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) |
57 |
30
|
fveq2d |
⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) = ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) |
58 |
40 55
|
jca |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) ) |
59 |
58
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) ) |
60 |
|
ovolfiniun |
⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ⊆ ℝ ∧ ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) |
61 |
45 59 60
|
syl2anc |
⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) |
62 |
57 61
|
eqbrtrd |
⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) |
63 |
|
ovollecl |
⊢ ( ( 𝐾 ⊆ ℝ ∧ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ∧ ( vol* ‘ 𝐾 ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑀 ) ( vol* ‘ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) → ( vol* ‘ 𝐾 ) ∈ ℝ ) |
64 |
44 56 62 63
|
syl3anc |
⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) ∈ ℝ ) |
65 |
30 64
|
jca |
⊢ ( 𝜑 → ( 𝐾 = ∪ 𝑗 ∈ ( 1 ... 𝑀 ) ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) ) |