Step | Hyp | Ref
| Expression |
1 | | ovncvrrp.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | ovncvrrp.n0 |
. . . 4
⊢ (𝜑 → 𝑋 ≠ ∅) |
3 | | ovncvrrp.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚
𝑋)) |
4 | | ovncvrrp.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
5 | | eqid 2622 |
. . . 4
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
6 | 1, 2, 3, 4, 5 | ovnlerp 40776 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
7 | | simp1 1061 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝜑) |
8 | | simp3 1063 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
9 | | rabid 3116 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ↔ (𝑧 ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
10 | 9 | biimpi 206 |
. . . . . . . . 9
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} → (𝑧 ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
11 | 10 | simprd 479 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
13 | 12 | 3adant1 1079 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
14 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑖(𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
15 | | nfe1 2027 |
. . . . . . . 8
⊢
Ⅎ𝑖∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
16 | | simp1l 1085 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝜑) |
17 | | simp2 1062 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
18 | | simp3l 1089 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
19 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → (𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
20 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑖 → (𝑙‘𝑗) = (𝑖‘𝑗)) |
21 | 20 | coeq2d 5284 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑖 → ([,) ∘ (𝑙‘𝑗)) = ([,) ∘ (𝑖‘𝑗))) |
22 | 21 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑖 → (([,) ∘ (𝑙‘𝑗))‘𝑘) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
23 | 22 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑖 → X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
24 | 23 | iuneq2d 4547 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑖 → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
25 | 24 | sseq2d 3633 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑖 → (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) ↔ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
26 | 25 | elrab 3363 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} ↔ (𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
27 | 19, 26 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝑖 ∈ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
28 | 27 | 3adant1 1079 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝑖 ∈ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
29 | | ovncvrrp.c |
. . . . . . . . . . . . . . . . 17
⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)})) |
31 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝐴 → (𝑎 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) ↔ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘))) |
32 | 31 | rabbidv 3189 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝐴 → {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
33 | 32 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
34 | | ovexd 6680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℝ
↑𝑚 𝑋) ∈ V) |
35 | 34, 3 | ssexd 4805 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ V) |
36 | | elpwg 4166 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↔ 𝐴 ⊆ (ℝ ↑𝑚
𝑋))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↔ 𝐴 ⊆ (ℝ ↑𝑚
𝑋))) |
38 | 3, 37 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋)) |
39 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∈
V |
40 | 39 | rabex 4813 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑙 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} ∈ V |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} ∈ V) |
42 | 30, 33, 38, 41 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶‘𝐴) = {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
43 | 42 | eqcomd 2628 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = (𝐶‘𝐴)) |
44 | 43 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = (𝐶‘𝐴)) |
45 | 28, 44 | eleqtrd 2703 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝑖 ∈ (𝐶‘𝐴)) |
46 | 16, 17, 18, 45 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑖 ∈ (𝐶‘𝐴)) |
47 | | ovncvrrp.l |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘))) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
𝐿 = (ℎ ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘)))) |
49 | | coeq2 5280 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ = (𝑖‘𝑗) → ([,) ∘ ℎ) = ([,) ∘ (𝑖‘𝑗))) |
50 | 49 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = (𝑖‘𝑗) → (([,) ∘ ℎ)‘𝑘) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
51 | 50 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = (𝑖‘𝑗) → (vol‘(([,) ∘ ℎ)‘𝑘)) = (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
52 | 51 | prodeq2ad 39824 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = (𝑖‘𝑗) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) ∧
ℎ = (𝑖‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
54 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) →
𝑖:ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋)) |
55 | 54 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
𝑖:ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋)) |
56 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
𝑗 ∈
ℕ) |
57 | 55, 56 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
(𝑖‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
58 | | prodex 14637 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
∏𝑘 ∈
𝑋 (vol‘(([,) ∘
(𝑖‘𝑗))‘𝑘)) ∈ V |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) ∈ V) |
60 | 48, 53, 57, 59 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
(𝐿‘(𝑖‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
61 | 60 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) →
(𝑗 ∈ ℕ ↦
(𝐿‘(𝑖‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) |
62 | 61 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
64 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) → 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
65 | 64 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = 𝑧) |
66 | 65 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = 𝑧) |
67 | 63, 66 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) = 𝑧) |
68 | 67 | 3adant1 1079 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) = 𝑧) |
69 | | simp1 1061 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
70 | 68, 69 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
71 | 70 | 3adant1l 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
72 | 71 | 3adant3l 1322 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
73 | 46, 72 | jca 554 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
74 | | 19.8a 2052 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
75 | 73, 74 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
76 | 75 | 3exp 1264 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → (𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) →
((𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))))) |
77 | 14, 15, 76 | rexlimd 3026 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → (∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))) |
78 | 77 | imp 445 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
79 | 7, 8, 13, 78 | syl21anc 1325 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
80 | 79 | 3exp 1264 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} → (𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))))) |
81 | 80 | rexlimdv 3030 |
. . 3
⊢ (𝜑 → (∃𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))) |
82 | 6, 81 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
83 | | rabid 3116 |
. . . . . . . 8
⊢ (𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ↔ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
84 | 83 | bicomi 214 |
. . . . . . 7
⊢ ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ↔ 𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
85 | 84 | biimpi 206 |
. . . . . 6
⊢ ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
86 | 85 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
87 | | ovncvrrp.d |
. . . . . . . . . 10
⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) |
88 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏(𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) |
89 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎ℝ+ |
90 | | nfv 1843 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑎(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒) |
91 | | nfmpt1 4747 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑎(𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
92 | 29, 91 | nfcxfr 2762 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑎𝐶 |
93 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑎𝑏 |
94 | 92, 93 | nffv 6198 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑎(𝐶‘𝑏) |
95 | 90, 94 | nfrab 3123 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎{𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)} |
96 | 89, 95 | nfmpt 4746 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎(𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) |
97 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (𝐶‘𝑎) = (𝐶‘𝑏)) |
98 | 97 | eleq2d 2687 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (𝑖 ∈ (𝐶‘𝑎) ↔ 𝑖 ∈ (𝐶‘𝑏))) |
99 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑏 → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘𝑏)) |
100 | 99 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)) |
101 | 100 | breq2d 4665 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒))) |
102 | 98, 101 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → ((𝑖 ∈ (𝐶‘𝑎) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘𝑏) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)))) |
103 | 102 | rabbidva2 3186 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) |
104 | 103 | mpteq2dv 4745 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)})) |
105 | 88, 96, 104 | cbvmpt 4749 |
. . . . . . . . . 10
⊢ (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) = (𝑏 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)})) |
106 | 87, 105 | eqtri 2644 |
. . . . . . . . 9
⊢ 𝐷 = (𝑏 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)})) |
107 | 106 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝐷 = (𝑏 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}))) |
108 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝐴 → (𝐶‘𝑏) = (𝐶‘𝐴)) |
109 | 108 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝐴 → (𝑖 ∈ (𝐶‘𝑏) ↔ 𝑖 ∈ (𝐶‘𝐴))) |
110 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝐴 → ((voln*‘𝑋)‘𝑏) = ((voln*‘𝑋)‘𝐴)) |
111 | 110 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝐴 → (((voln*‘𝑋)‘𝑏) +𝑒 𝑒) = (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)) |
112 | 111 | breq2d 4665 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝐴 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒))) |
113 | 109, 112 | anbi12d 747 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐴 → ((𝑖 ∈ (𝐶‘𝑏) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)))) |
114 | 113 | rabbidva2 3186 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐴 → {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)}) |
115 | 114 | mpteq2dv 4745 |
. . . . . . . . 9
⊢ (𝑏 = 𝐴 → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)})) |
116 | 115 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) ∧ 𝑏 = 𝐴) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)})) |
117 | 38 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋)) |
118 | | rpex 39562 |
. . . . . . . . . 10
⊢
ℝ+ ∈ V |
119 | 118 | mptex 6486 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ+
↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)}) ∈ V |
120 | 119 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)}) ∈ V) |
121 | 107, 116,
117, 120 | fvmptd 6288 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → (𝐷‘𝐴) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)})) |
122 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐸 → (((voln*‘𝑋)‘𝐴) +𝑒 𝑒) = (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
123 | 122 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
124 | 123 | rabbidv 3189 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
125 | 124 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) ∧ 𝑒 = 𝐸) → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
126 | 4 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝐸 ∈
ℝ+) |
127 | | fvex 6201 |
. . . . . . . . 9
⊢ (𝐶‘𝐴) ∈ V |
128 | 127 | rabex 4813 |
. . . . . . . 8
⊢ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ∈ V |
129 | 128 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ∈ V) |
130 | 121, 125,
126, 129 | fvmptd 6288 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → ((𝐷‘𝐴)‘𝐸) = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
131 | 130 | eqcomd 2628 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} = ((𝐷‘𝐴)‘𝐸)) |
132 | 86, 131 | eleqtrd 2703 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝑖 ∈ ((𝐷‘𝐴)‘𝐸)) |
133 | 132 | ex 450 |
. . 3
⊢ (𝜑 → ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝑖 ∈ ((𝐷‘𝐴)‘𝐸))) |
134 | 133 | eximdv 1846 |
. 2
⊢ (𝜑 → (∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝐸))) |
135 | 82, 134 | mpd 15 |
1
⊢ (𝜑 → ∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝐸)) |