Step | Hyp | Ref
| Expression |
1 | | ovnlecvr.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | ovnlecvr.n0 |
. . 3
⊢ (𝜑 → 𝑋 ≠ ∅) |
3 | | ovnlecvr.ss |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
4 | | ovnlecvr.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ)
↑𝑚 𝑋)) |
5 | 4 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
6 | | elmapi 7879 |
. . . . . . . 8
⊢ ((𝐼‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋) → (𝐼‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
8 | 7 | hoissrrn 40763 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘) ⊆ (ℝ ↑𝑚
𝑋)) |
9 | 8 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘) ⊆ (ℝ ↑𝑚
𝑋)) |
10 | | iunss 4561 |
. . . . 5
⊢ (∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘) ⊆ (ℝ ↑𝑚
𝑋) ↔ ∀𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘) ⊆ (ℝ ↑𝑚
𝑋)) |
11 | 9, 10 | sylibr 224 |
. . . 4
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘) ⊆ (ℝ ↑𝑚
𝑋)) |
12 | 3, 11 | sstrd 3613 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚
𝑋)) |
13 | | eqid 2622 |
. . 3
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
14 | 1, 2, 12, 13 | ovnn0val 40765 |
. 2
⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
)) |
15 | | ssrab2 3687 |
. . . 4
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆
ℝ* |
16 | 15 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆
ℝ*) |
17 | | nnex 11026 |
. . . . . . 7
⊢ ℕ
∈ V |
18 | 17 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℕ ∈
V) |
19 | | icossicc 12260 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
20 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ ℕ) |
21 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin) |
22 | | ovnlecvr.l |
. . . . . . . . 9
⊢ 𝐿 = (𝑖 ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘))) |
23 | 20, 21, 22, 7 | hoiprodcl2 40769 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐿‘(𝐼‘𝑗)) ∈ (0[,)+∞)) |
24 | 19, 23 | sseldi 3601 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐿‘(𝐼‘𝑗)) ∈ (0[,]+∞)) |
25 | | eqid 2622 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗))) |
26 | 24, 25 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗))):ℕ⟶(0[,]+∞)) |
27 | 18, 26 | sge0xrcl 40602 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) ∈
ℝ*) |
28 | | ovex 6678 |
. . . . . . . . 9
⊢ ((ℝ
× ℝ) ↑𝑚 𝑋) ∈ V |
29 | 28, 17 | pm3.2i 471 |
. . . . . . . 8
⊢
(((ℝ × ℝ) ↑𝑚 𝑋) ∈ V ∧ ℕ ∈
V) |
30 | | elmapg 7870 |
. . . . . . . 8
⊢
((((ℝ × ℝ) ↑𝑚 𝑋) ∈ V ∧ ℕ ∈
V) → (𝐼 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ↔
𝐼:ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋))) |
31 | 29, 30 | ax-mp 5 |
. . . . . . 7
⊢ (𝐼 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ↔
𝐼:ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋)) |
32 | 4, 31 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
33 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐿 = (𝑖 ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))) |
34 | | coeq2 5280 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝐼‘𝑗) → ([,) ∘ 𝑖) = ([,) ∘ (𝐼‘𝑗))) |
35 | 34 | fveq1d 6193 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝐼‘𝑗) → (([,) ∘ 𝑖)‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
36 | 35 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝐼‘𝑗) → (vol‘(([,) ∘ 𝑖)‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
37 | 36 | prodeq2ad 39824 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝐼‘𝑗) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
38 | 37 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑖 = (𝐼‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
39 | | prodex 14637 |
. . . . . . . . . . 11
⊢
∏𝑘 ∈
𝑋 (vol‘(([,) ∘
(𝐼‘𝑗))‘𝑘)) ∈ V |
40 | 39 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) ∈ V) |
41 | 33, 38, 5, 40 | fvmptd 6288 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐿‘(𝐼‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
42 | 41 | mpteq2dva 4744 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))) |
43 | 42 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) |
44 | 3, 43 | jca 554 |
. . . . . 6
⊢ (𝜑 → (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) |
45 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘 𝑖 = 𝐼 |
46 | | fveq1 6190 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝐼 → (𝑖‘𝑗) = (𝐼‘𝑗)) |
47 | 46 | coeq2d 5284 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝐼 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗))) |
48 | 47 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
49 | 48 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
50 | 45, 49 | ixpeq2d 39237 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
51 | 50 | iuneq2d 4547 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
52 | 51 | sseq2d 3633 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘))) |
53 | 48 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
54 | 53 | prodeq2ad 39824 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
55 | 54 | mpteq2dv 4745 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))) |
56 | 55 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) |
57 | 56 | eqeq2d 2632 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) |
58 | 52, 57 | anbi12d 747 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → ((𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))) |
59 | 58 | rspcev 3309 |
. . . . . 6
⊢ ((𝐼 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
60 | 32, 44, 59 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
61 | 27, 60 | jca 554 |
. . . 4
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
62 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) → (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
63 | 62 | anbi2d 740 |
. . . . . 6
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) → ((𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
64 | 63 | rexbidv 3052 |
. . . . 5
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) → (∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
65 | 64 | elrab 3363 |
. . . 4
⊢
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ↔
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
66 | 61, 65 | sylibr 224 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
67 | | infxrlb 12164 |
. . 3
⊢ (({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆ ℝ* ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗))))) |
68 | 16, 66, 67 | syl2anc 693 |
. 2
⊢ (𝜑 → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗))))) |
69 | 14, 68 | eqbrtrd 4675 |
1
⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗))))) |