Step | Hyp | Ref
| Expression |
1 | | ovncvrrp.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | ovncvrrp.n0 |
. . . 4
⊢ (𝜑 → 𝑋 ≠ ∅) |
3 | | ovncvrrp.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚
𝑋)) |
4 | | ovncvrrp.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
5 | | eqid 2610 |
. . . 4
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
6 | 1, 2, 3, 4, 5 | ovnlerp 39452 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
7 | | simp1 1054 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝜑) |
8 | | simp3 1056 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
9 | | rabid 3095 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ↔ (𝑧 ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
10 | 9 | biimpi 205 |
. . . . . . . . 9
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} → (𝑧 ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
11 | 10 | simprd 478 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
13 | 12 | 3adant1 1072 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
14 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑖(𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
15 | | nfe1 2014 |
. . . . . . . 8
⊢
Ⅎ𝑖∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
16 | | simp1l 1078 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝜑) |
17 | | simp2 1055 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
18 | | simp3l 1082 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
19 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → (𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
20 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑖 → (𝑙‘𝑗) = (𝑖‘𝑗)) |
21 | 20 | coeq2d 5206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑖 → ([,) ∘ (𝑙‘𝑗)) = ([,) ∘ (𝑖‘𝑗))) |
22 | 21 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑖 → (([,) ∘ (𝑙‘𝑗))‘𝑘) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
23 | 22 | ixpeq2dv 7810 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑖 → X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
24 | 23 | iuneq2d 4483 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑖 → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
25 | 24 | sseq2d 3596 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑖 → (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) ↔ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
26 | 25 | elrab 3331 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} ↔ (𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
27 | 19, 26 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝑖 ∈ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
28 | 27 | 3adant1 1072 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝑖 ∈ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
29 | | ovncvrrp.c |
. . . . . . . . . . . . . . . . 17
⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)})) |
31 | | sseq1 3589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝐴 → (𝑎 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) ↔ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘))) |
32 | 31 | rabbidv 3164 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝐴 → {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
33 | 32 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
34 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℝ
↑𝑚 𝑋) ∈ V |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℝ
↑𝑚 𝑋) ∈ V) |
36 | 35, 3 | ssexd 4733 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ V) |
37 | | elpwg 4116 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↔ 𝐴 ⊆ (ℝ ↑𝑚
𝑋))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↔ 𝐴 ⊆ (ℝ ↑𝑚
𝑋))) |
39 | 3, 38 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋)) |
40 | | ovex 6577 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∈
V |
41 | 40 | rabex 4740 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑙 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} ∈ V |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} ∈ V) |
43 | 30, 33, 39, 42 | fvmptd 6197 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶‘𝐴) = {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
44 | 43 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = (𝐶‘𝐴)) |
45 | 44 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = (𝐶‘𝐴)) |
46 | 28, 45 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝑖 ∈ (𝐶‘𝐴)) |
47 | 16, 17, 18, 46 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑖 ∈ (𝐶‘𝐴)) |
48 | | ovncvrrp.l |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘))) |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
𝐿 = (ℎ ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘)))) |
50 | | coeq2 5202 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ = (𝑖‘𝑗) → ([,) ∘ ℎ) = ([,) ∘ (𝑖‘𝑗))) |
51 | 50 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = (𝑖‘𝑗) → (([,) ∘ ℎ)‘𝑘) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
52 | 51 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = (𝑖‘𝑗) → (vol‘(([,) ∘ ℎ)‘𝑘)) = (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
53 | 52 | prodeq2ad 38659 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = (𝑖‘𝑗) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
54 | 53 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) ∧
ℎ = (𝑖‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
55 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) →
𝑖:ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋)) |
56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
𝑖:ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋)) |
57 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
𝑗 ∈
ℕ) |
58 | 56, 57 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
(𝑖‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
59 | | prodex 14476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
∏𝑘 ∈
𝑋 (vol‘(([,) ∘
(𝑖‘𝑗))‘𝑘)) ∈ V |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) ∈ V) |
61 | 49, 54, 58, 60 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑗 ∈ ℕ) →
(𝐿‘(𝑖‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
62 | 61 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) →
(𝑗 ∈ ℕ ↦
(𝐿‘(𝑖‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
65 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) → 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
66 | 65 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = 𝑧) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = 𝑧) |
68 | 64, 67 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) = 𝑧) |
69 | 68 | 3adant1 1072 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) = 𝑧) |
70 | | simp1 1054 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
71 | 69, 70 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
72 | 71 | 3adant1l 1310 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
73 | 72 | 3adant3l 1314 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
74 | 47, 73 | jca 553 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
75 | | 19.8a 2039 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
76 | 74, 75 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
77 | 76 | 3exp 1256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → (𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) →
((𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))))) |
78 | 14, 15, 77 | rexlimd 3008 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → (∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))) |
79 | 78 | imp 444 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
80 | 7, 8, 13, 79 | syl21anc 1317 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
81 | 80 | 3exp 1256 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} → (𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))))) |
82 | 81 | rexlimdv 3012 |
. . 3
⊢ (𝜑 → (∃𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))) |
83 | 6, 82 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
84 | | rabid 3095 |
. . . . . . . 8
⊢ (𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ↔ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
85 | 84 | bicomi 213 |
. . . . . . 7
⊢ ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ↔ 𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
86 | 85 | biimpi 205 |
. . . . . 6
⊢ ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
87 | 86 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
88 | | ovncvrrp.d |
. . . . . . . . . 10
⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) |
89 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏(𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) |
90 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎ℝ+ |
91 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑎(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒) |
92 | | nfmpt1 4675 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑎(𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
93 | 29, 92 | nfcxfr 2749 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑎𝐶 |
94 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑎𝑏 |
95 | 93, 94 | nffv 6110 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑎(𝐶‘𝑏) |
96 | 91, 95 | nfrab 3100 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎{𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)} |
97 | 90, 96 | nfmpt 4674 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎(𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) |
98 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (𝐶‘𝑎) = (𝐶‘𝑏)) |
99 | 98 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (𝑖 ∈ (𝐶‘𝑎) ↔ 𝑖 ∈ (𝐶‘𝑏))) |
100 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑏 → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘𝑏)) |
101 | 100 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)) |
102 | 101 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒))) |
103 | 99, 102 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → ((𝑖 ∈ (𝐶‘𝑎) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘𝑏) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)))) |
104 | 103 | rabbidva2 3162 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) |
105 | 104 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)})) |
106 | 89, 97, 105 | cbvmpt 4677 |
. . . . . . . . . 10
⊢ (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) = (𝑏 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)})) |
107 | 88, 106 | eqtri 2632 |
. . . . . . . . 9
⊢ 𝐷 = (𝑏 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)})) |
108 | 107 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝐷 = (𝑏 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}))) |
109 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝐴 → (𝐶‘𝑏) = (𝐶‘𝐴)) |
110 | 109 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝐴 → (𝑖 ∈ (𝐶‘𝑏) ↔ 𝑖 ∈ (𝐶‘𝐴))) |
111 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝐴 → ((voln*‘𝑋)‘𝑏) = ((voln*‘𝑋)‘𝐴)) |
112 | 111 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝐴 → (((voln*‘𝑋)‘𝑏) +𝑒 𝑒) = (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)) |
113 | 112 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝐴 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒))) |
114 | 110, 113 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐴 → ((𝑖 ∈ (𝐶‘𝑏) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)))) |
115 | 114 | rabbidva2 3162 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐴 → {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)}) |
116 | 115 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝑏 = 𝐴 → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)})) |
117 | 116 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) ∧ 𝑏 = 𝐴) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)})) |
118 | 39 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋)) |
119 | | rpex 38503 |
. . . . . . . . . 10
⊢
ℝ+ ∈ V |
120 | 119 | mptex 6390 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ+
↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)}) ∈ V |
121 | 120 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)}) ∈ V) |
122 | 108, 117,
118, 121 | fvmptd 6197 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → (𝐷‘𝐴) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)})) |
123 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐸 → (((voln*‘𝑋)‘𝐴) +𝑒 𝑒) = (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
124 | 123 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
125 | 124 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
126 | 125 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) ∧ 𝑒 = 𝐸) → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
127 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝐸 ∈
ℝ+) |
128 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐶‘𝐴) ∈ V |
129 | 128 | rabex 4740 |
. . . . . . . 8
⊢ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ∈ V |
130 | 129 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ∈ V) |
131 | 122, 126,
127, 130 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → ((𝐷‘𝐴)‘𝐸) = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
132 | 131 | eqcomd 2616 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} = ((𝐷‘𝐴)‘𝐸)) |
133 | 87, 132 | eleqtrd 2690 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝑖 ∈ ((𝐷‘𝐴)‘𝐸)) |
134 | 133 | ex 449 |
. . 3
⊢ (𝜑 → ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝑖 ∈ ((𝐷‘𝐴)‘𝐸))) |
135 | 134 | eximdv 1833 |
. 2
⊢ (𝜑 → (∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝐸))) |
136 | 83, 135 | mpd 15 |
1
⊢ (𝜑 → ∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝐸)) |