Step | Hyp | Ref
| Expression |
1 | | ovncvrrp.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | ovncvrrp.n0 |
. . . 4
⊢ (𝜑 → 𝑋 ≠ ∅) |
3 | | ovncvrrp.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) |
4 | | ovncvrrp.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
5 | | eqid 2739 |
. . . 4
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
6 | 1, 2, 3, 4, 5 | ovnlerp 43683 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
7 | | simp1 1137 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝜑) |
8 | | simp3 1139 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
9 | | rabid 3282 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ↔ (𝑧 ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
10 | 9 | biimpi 219 |
. . . . . . . . 9
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} → (𝑧 ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
11 | 10 | simprd 499 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} → ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
12 | 11 | adantr 484 |
. . . . . . 7
⊢ ((𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
13 | 12 | 3adant1 1131 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
14 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑖(𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
15 | | nfe1 2155 |
. . . . . . . 8
⊢
Ⅎ𝑖∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
16 | | simp1l 1198 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝜑) |
17 | | simp2 1138 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) |
18 | | simp3l 1202 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
19 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → (𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
20 | | fveq1 6686 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑖 → (𝑙‘𝑗) = (𝑖‘𝑗)) |
21 | 20 | coeq2d 5715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑖 → ([,) ∘ (𝑙‘𝑗)) = ([,) ∘ (𝑖‘𝑗))) |
22 | 21 | fveq1d 6689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑖 → (([,) ∘ (𝑙‘𝑗))‘𝑘) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
23 | 22 | ixpeq2dv 8536 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑖 → X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
24 | 23 | iuneq2d 4920 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑖 → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
25 | 24 | sseq2d 3919 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑖 → (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) ↔ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
26 | 25 | elrab 3593 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ {𝑙 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∣ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} ↔ (𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
27 | 19, 26 | sylibr 237 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝑖 ∈ {𝑙 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∣ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
28 | 27 | 3adant1 1131 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝑖 ∈ {𝑙 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∣ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
29 | | ovncvrrp.c |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m
𝑋) ↦ {𝑙 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
30 | | sseq1 3912 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝐴 → (𝑎 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘) ↔ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘))) |
31 | 30 | rabbidv 3382 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝐴 → {𝑙 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∣ 𝑎 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = {𝑙 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∣ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
32 | | ovexd 7218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℝ
↑m 𝑋)
∈ V) |
33 | 32, 3 | ssexd 5202 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ V) |
34 | | elpwg 4501 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 (ℝ
↑m 𝑋)
↔ 𝐴 ⊆ (ℝ
↑m 𝑋))) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ 𝒫 (ℝ
↑m 𝑋)
↔ 𝐴 ⊆ (ℝ
↑m 𝑋))) |
36 | 3, 35 | mpbird 260 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ 𝒫 (ℝ
↑m 𝑋)) |
37 | | ovex 7216 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∈
V |
38 | 37 | rabex 5210 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑙 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} ∈ V |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑙 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∣ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} ∈ V) |
40 | 29, 31, 36, 39 | fvmptd3 6811 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶‘𝐴) = {𝑙 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∣ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
41 | 40 | eqcomd 2745 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑙 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∣ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = (𝐶‘𝐴)) |
42 | 41 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → {𝑙 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∣ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)} = (𝐶‘𝐴)) |
43 | 28, 42 | eleqtrd 2836 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝑖 ∈ (𝐶‘𝐴)) |
44 | 16, 17, 18, 43 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑖 ∈ (𝐶‘𝐴)) |
45 | | ovncvrrp.l |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ)
↑m 𝑋)
↦ ∏𝑘 ∈
𝑋 (vol‘(([,) ∘
ℎ)‘𝑘))) |
46 | | coeq2 5711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = (𝑖‘𝑗) → ([,) ∘ ℎ) = ([,) ∘ (𝑖‘𝑗))) |
47 | 46 | fveq1d 6689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = (𝑖‘𝑗) → (([,) ∘ ℎ)‘𝑘) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
48 | 47 | fveq2d 6691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = (𝑖‘𝑗) → (vol‘(([,) ∘ ℎ)‘𝑘)) = (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
49 | 48 | prodeq2ad 42716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = (𝑖‘𝑗) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
50 | | elmapi 8472 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → 𝑖:ℕ⟶((ℝ
× ℝ) ↑m 𝑋)) |
51 | 50 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) → 𝑖:ℕ⟶((ℝ
× ℝ) ↑m 𝑋)) |
52 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ) |
53 | 51, 52 | ffvelrnd 6875 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) → (𝑖‘𝑗) ∈ ((ℝ × ℝ)
↑m 𝑋)) |
54 | | prodex 15366 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
∏𝑘 ∈
𝑋 (vol‘(([,) ∘
(𝑖‘𝑗))‘𝑘)) ∈ V |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) →
∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) ∈ V) |
56 | 45, 49, 53, 55 | fvmptd3 6811 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘(𝑖‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) |
57 | 56 | mpteq2dva 5135 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) |
58 | 57 | fveq2d 6691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
59 | 58 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
60 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) → 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
61 | 60 | eqcomd 2745 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = 𝑧) |
62 | 61 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) = 𝑧) |
63 | 59, 62 | eqtrd 2774 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) = 𝑧) |
64 | 63 | 3adant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) = 𝑧) |
65 | | simp1 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
66 | 64, 65 | eqbrtrd 5062 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
67 | 66 | 3adant1l 1177 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
68 | 67 | 3adant3l 1181 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
69 | 44, 68 | jca 515 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
70 | 69 | 19.8ad 2183 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
71 | 70 | 3exp 1120 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → (𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) → ((𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))))) |
72 | 14, 15, 71 | rexlimd 3228 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → (∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))) |
73 | 72 | imp 410 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ∧ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
74 | 7, 8, 13, 73 | syl21anc 837 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∧ 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
75 | 74 | 3exp 1120 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} → (𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))))) |
76 | 75 | rexlimdv 3194 |
. . 3
⊢ (𝜑 → (∃𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸) → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)))) |
77 | 6, 76 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
78 | | rabid 3282 |
. . . . . . . 8
⊢ (𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ↔ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
79 | 78 | bicomi 227 |
. . . . . . 7
⊢ ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) ↔ 𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
80 | 79 | biimpi 219 |
. . . . . 6
⊢ ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
81 | 80 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝑖 ∈ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
82 | | ovncvrrp.d |
. . . . . . . . 9
⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m
𝑋) ↦ (𝑒 ∈ ℝ+
↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) |
83 | | nfcv 2900 |
. . . . . . . . . 10
⊢
Ⅎ𝑏(𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) |
84 | | nfcv 2900 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎ℝ+ |
85 | | nfv 1921 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒) |
86 | | nfmpt1 5138 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑎(𝑎 ∈ 𝒫 (ℝ ↑m
𝑋) ↦ {𝑙 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) |
87 | 29, 86 | nfcxfr 2898 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑎𝐶 |
88 | | nfcv 2900 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑎𝑏 |
89 | 87, 88 | nffv 6697 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎(𝐶‘𝑏) |
90 | 85, 89 | nfrabw 3289 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎{𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)} |
91 | 84, 90 | nfmpt 5137 |
. . . . . . . . . 10
⊢
Ⅎ𝑎(𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) |
92 | | fveq2 6687 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (𝐶‘𝑎) = (𝐶‘𝑏)) |
93 | 92 | eleq2d 2819 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 → (𝑖 ∈ (𝐶‘𝑎) ↔ 𝑖 ∈ (𝐶‘𝑏))) |
94 | | fveq2 6687 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘𝑏)) |
95 | 94 | oveq1d 7198 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)) |
96 | 95 | breq2d 5052 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑏 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒))) |
97 | 93, 96 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → ((𝑖 ∈ (𝐶‘𝑎) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘𝑏) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)))) |
98 | 97 | rabbidva2 3378 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) |
99 | 98 | mpteq2dv 5136 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)})) |
100 | 83, 91, 99 | cbvmpt 5141 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝒫 (ℝ
↑m 𝑋)
↦ (𝑒 ∈
ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) = (𝑏 ∈ 𝒫 (ℝ ↑m
𝑋) ↦ (𝑒 ∈ ℝ+
↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)})) |
101 | 82, 100 | eqtri 2762 |
. . . . . . . 8
⊢ 𝐷 = (𝑏 ∈ 𝒫 (ℝ ↑m
𝑋) ↦ (𝑒 ∈ ℝ+
↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)})) |
102 | | fveq2 6687 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝐴 → (𝐶‘𝑏) = (𝐶‘𝐴)) |
103 | 102 | eleq2d 2819 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐴 → (𝑖 ∈ (𝐶‘𝑏) ↔ 𝑖 ∈ (𝐶‘𝐴))) |
104 | | fveq2 6687 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝐴 → ((voln*‘𝑋)‘𝑏) = ((voln*‘𝑋)‘𝐴)) |
105 | 104 | oveq1d 7198 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝐴 → (((voln*‘𝑋)‘𝑏) +𝑒 𝑒) = (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)) |
106 | 105 | breq2d 5052 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐴 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒))) |
107 | 103, 106 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐴 → ((𝑖 ∈ (𝐶‘𝑏) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)))) |
108 | 107 | rabbidva2 3378 |
. . . . . . . . 9
⊢ (𝑏 = 𝐴 → {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)}) |
109 | 108 | mpteq2dv 5136 |
. . . . . . . 8
⊢ (𝑏 = 𝐴 → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑏) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑏) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)})) |
110 | 36 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝐴 ∈ 𝒫 (ℝ
↑m 𝑋)) |
111 | | rpex 42464 |
. . . . . . . . . 10
⊢
ℝ+ ∈ V |
112 | 111 | mptex 7009 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℝ+
↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)}) ∈ V |
113 | 112 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)}) ∈ V) |
114 | 101, 109,
110, 113 | fvmptd3 6811 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → (𝐷‘𝐴) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)})) |
115 | | oveq2 7191 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐸 → (((voln*‘𝑋)‘𝐴) +𝑒 𝑒) = (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) |
116 | 115 | breq2d 5052 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) |
117 | 116 | rabbidv 3382 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
118 | 117 | adantl 485 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) ∧ 𝑒 = 𝐸) → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
119 | 4 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝐸 ∈
ℝ+) |
120 | | fvex 6700 |
. . . . . . . . 9
⊢ (𝐶‘𝐴) ∈ V |
121 | 120 | rabex 5210 |
. . . . . . . 8
⊢ {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ∈ V |
122 | 121 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} ∈ V) |
123 | 114, 118,
119, 122 | fvmptd 6795 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → ((𝐷‘𝐴)‘𝐸) = {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)}) |
124 | 123 | eqcomd 2745 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → {𝑖 ∈ (𝐶‘𝐴) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)} = ((𝐷‘𝐴)‘𝐸)) |
125 | 81, 124 | eleqtrd 2836 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) → 𝑖 ∈ ((𝐷‘𝐴)‘𝐸)) |
126 | 125 | ex 416 |
. . 3
⊢ (𝜑 → ((𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → 𝑖 ∈ ((𝐷‘𝐴)‘𝐸))) |
127 | 126 | eximdv 1924 |
. 2
⊢ (𝜑 → (∃𝑖(𝑖 ∈ (𝐶‘𝐴) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) → ∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝐸))) |
128 | 77, 127 | mpd 15 |
1
⊢ (𝜑 → ∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝐸)) |