Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . 6
⊢ (𝑋 = ∅ →
(voln*‘𝑋) =
(voln*‘∅)) |
2 | 1 | fveq1d 6105 |
. . . . 5
⊢ (𝑋 = ∅ →
((voln*‘𝑋)‘𝐴) = ((voln*‘∅)‘𝐴)) |
3 | 2 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐴) = ((voln*‘∅)‘𝐴)) |
4 | | ovnlecvr2.s |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
6 | | 1nn 10908 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
7 | | ne0i 3880 |
. . . . . . . . . . 11
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . 10
⊢ ℕ
≠ ∅ |
9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℕ ≠
∅) |
10 | | iunconst 4465 |
. . . . . . . . 9
⊢ (ℕ
≠ ∅ → ∪ 𝑗 ∈ ℕ {∅} =
{∅}) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ {∅} =
{∅}) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∪ 𝑗 ∈ ℕ {∅} =
{∅}) |
13 | | ixpeq1 7805 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ ∅ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
14 | | ixp0x 7822 |
. . . . . . . . . . . 12
⊢ X𝑘 ∈
∅ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = {∅} |
15 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → X𝑘 ∈
∅ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = {∅}) |
16 | 13, 15 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = {∅}) |
17 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 = ∅ ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = {∅}) |
18 | 17 | iuneq2dv 4478 |
. . . . . . . 8
⊢ (𝑋 = ∅ → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪
𝑗 ∈ ℕ
{∅}) |
19 | 18 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪
𝑗 ∈ ℕ
{∅}) |
20 | | reex 9906 |
. . . . . . . . 9
⊢ ℝ
∈ V |
21 | | mapdm0 38378 |
. . . . . . . . 9
⊢ (ℝ
∈ V → (ℝ ↑𝑚 ∅) =
{∅}) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . 8
⊢ (ℝ
↑𝑚 ∅) = {∅} |
23 | 22 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → (ℝ
↑𝑚 ∅) = {∅}) |
24 | 12, 19, 23 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (ℝ ↑𝑚
∅)) |
25 | 5, 24 | sseqtrd 3604 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴 ⊆ (ℝ ↑𝑚
∅)) |
26 | 25 | ovn0val 39440 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) →
((voln*‘∅)‘𝐴) = 0) |
27 | 3, 26 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐴) = 0) |
28 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑗𝜑 |
29 | | nnex 10903 |
. . . . . 6
⊢ ℕ
∈ V |
30 | 29 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℕ ∈
V) |
31 | | icossicc 12131 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
32 | | ovnlecvr2.l |
. . . . . . 7
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
33 | | ovnlecvr2.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ Fin) |
34 | 33 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin) |
35 | | ovnlecvr2.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶:ℕ⟶(ℝ
↑𝑚 𝑋)) |
36 | 35 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑋)) |
37 | | elmapi 7765 |
. . . . . . . 8
⊢ ((𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑋) → (𝐶‘𝑗):𝑋⟶ℝ) |
38 | 36, 37 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ) |
39 | | ovnlecvr2.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷:ℕ⟶(ℝ
↑𝑚 𝑋)) |
40 | 39 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑋)) |
41 | | elmapi 7765 |
. . . . . . . 8
⊢ ((𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑋) → (𝐷‘𝑗):𝑋⟶ℝ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) |
43 | 32, 34, 38, 42 | hoidmvcl 39472 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞)) |
44 | 31, 43 | sseldi 3566 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞)) |
45 | 28, 30, 44 | sge0ge0mpt 39331 |
. . . 4
⊢ (𝜑 → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
46 | 45 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
47 | 27, 46 | eqbrtrd 4605 |
. 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
48 | | simpl 472 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝜑) |
49 | | neqne 2790 |
. . . 4
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
50 | 49 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
51 | 33 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ∈ Fin) |
52 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ≠ ∅) |
53 | 38 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ) |
54 | 42 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ) |
55 | 54 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈
ℝ*) |
56 | | icossre 12125 |
. . . . . . . . . . . . 13
⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ*) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ) |
57 | 53, 55, 56 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ) |
58 | 57 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ) |
59 | | ss2ixp 7807 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ℝ) |
60 | 58, 59 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ℝ) |
61 | 20 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈
V) |
62 | | ixpconstg 7803 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ Fin ∧ ℝ ∈
V) → X𝑘 ∈ 𝑋 ℝ = (ℝ
↑𝑚 𝑋)) |
63 | 33, 61, 62 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → X𝑘 ∈
𝑋 ℝ = (ℝ
↑𝑚 𝑋)) |
64 | 63 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 ℝ = (ℝ
↑𝑚 𝑋)) |
65 | 60, 64 | sseqtrd 3604 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ (ℝ
↑𝑚 𝑋)) |
66 | 65 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ (ℝ
↑𝑚 𝑋)) |
67 | | iunss 4497 |
. . . . . . . 8
⊢ (∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ (ℝ
↑𝑚 𝑋) ↔ ∀𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ (ℝ
↑𝑚 𝑋)) |
68 | 66, 67 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ (ℝ
↑𝑚 𝑋)) |
69 | 4, 68 | sstrd 3578 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚
𝑋)) |
70 | 69 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐴 ⊆ (ℝ ↑𝑚
𝑋)) |
71 | | eqid 2610 |
. . . . 5
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
72 | 51, 52, 70, 71 | ovnn0val 39441 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln*‘𝑋)‘𝐴) = inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
)) |
73 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆
ℝ* |
74 | 73 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆
ℝ*) |
75 | 28, 30, 44 | sge0xrclmpt 39321 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈
ℝ*) |
76 | 75 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈
ℝ*) |
77 | | opelxpi 5072 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ) → 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉 ∈ (ℝ ×
ℝ)) |
78 | 53, 54, 77 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉 ∈ (ℝ ×
ℝ)) |
79 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) |
80 | 78, 79 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉):𝑋⟶(ℝ ×
ℝ)) |
81 | 20, 20 | xpex 6860 |
. . . . . . . . . . . . . 14
⊢ (ℝ
× ℝ) ∈ V |
82 | 81 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℝ ×
ℝ) ∈ V) |
83 | | elmapg 7757 |
. . . . . . . . . . . . 13
⊢
(((ℝ × ℝ) ∈ V ∧ 𝑋 ∈ Fin) → ((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↔ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉):𝑋⟶(ℝ ×
ℝ))) |
84 | 82, 34, 83 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↔ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉):𝑋⟶(ℝ ×
ℝ))) |
85 | 80, 84 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
86 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
87 | 85, 86 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)):ℕ⟶((ℝ ×
ℝ) ↑𝑚 𝑋)) |
88 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ ((ℝ
× ℝ) ↑𝑚 𝑋) ∈ V |
89 | 88 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℝ × ℝ)
↑𝑚 𝑋) ∈ V) |
90 | | elmapg 7757 |
. . . . . . . . . . 11
⊢
((((ℝ × ℝ) ↑𝑚 𝑋) ∈ V ∧ ℕ ∈
V) → ((𝑗 ∈
ℕ ↦ (𝑘 ∈
𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ↔
(𝑗 ∈ ℕ ↦
(𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)):ℕ⟶((ℝ ×
ℝ) ↑𝑚 𝑋))) |
91 | 89, 30, 90 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ↔
(𝑗 ∈ ℕ ↦
(𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)):ℕ⟶((ℝ ×
ℝ) ↑𝑚 𝑋))) |
92 | 87, 91 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
93 | 92 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
94 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
95 | | mptexg 6389 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑋 ∈ Fin → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ V) |
96 | 33, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ V) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ V) |
98 | 86 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ ∧ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ V) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗) = (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
99 | 94, 97, 98 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗) = (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
100 | 99 | coeq2d 5206 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗)) = ([,) ∘ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))) |
101 | 100 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) = (([,) ∘ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑘)) |
102 | 101 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) = (([,) ∘ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑘)) |
103 | 80 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉):𝑋⟶(ℝ ×
ℝ)) |
104 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
105 | 103, 104 | fvovco 38376 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑘) = ((1st ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘))[,)(2nd ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘)))) |
106 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
107 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . 20
⊢
〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉 ∈ V |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉 ∈ V) |
109 | 79 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ 𝑋 ∧ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉 ∈ V) → ((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘) = 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) |
110 | 106, 108,
109 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘) = 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) |
111 | 110 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘)) = (1st ‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
112 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶‘𝑗)‘𝑘) ∈ V |
113 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷‘𝑗)‘𝑘) ∈ V |
114 | | op1stg 7071 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶‘𝑗)‘𝑘) ∈ V ∧ ((𝐷‘𝑗)‘𝑘) ∈ V) → (1st
‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = ((𝐶‘𝑗)‘𝑘)) |
115 | 112, 113,
114 | mp2an 704 |
. . . . . . . . . . . . . . . . . 18
⊢
(1st ‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = ((𝐶‘𝑗)‘𝑘) |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1st
‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = ((𝐶‘𝑗)‘𝑘)) |
117 | 111, 116 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘)) = ((𝐶‘𝑗)‘𝑘)) |
118 | 110 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘)) = (2nd ‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
119 | 112, 113 | op2nd 7068 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = ((𝐷‘𝑗)‘𝑘) |
120 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (2nd
‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = ((𝐷‘𝑗)‘𝑘)) |
121 | 118, 120 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘)) = ((𝐷‘𝑗)‘𝑘)) |
122 | 117, 121 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((1st ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘))[,)(2nd ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘))) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
123 | 122 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((1st ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘))[,)(2nd ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘))) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
124 | 102, 105,
123 | 3eqtrrd 2649 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
125 | 124 | ixpeq2dva 7809 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
126 | 125 | iuneq2dv 4478 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
127 | 4, 126 | sseqtrd 3604 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
128 | 127 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
129 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))) |
130 | 51 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin) |
131 | 52 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅) |
132 | 38 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ) |
133 | 42 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) |
134 | 32, 130, 131, 132, 133 | hoidmvn0val 39474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
135 | 134 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) |
136 | 135 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))) |
137 | 124 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
138 | 137 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
139 | 138 | prodeq2dv 14492 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
140 | 139 | mpteq2dva 4672 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) |
141 | 140 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))) |
142 | 141 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))) |
143 | 129, 136,
142 | 3eqtr4d 2654 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))))) |
144 | 128, 143 | jca 553 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))))) |
145 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝑖 |
146 | | nfmpt1 4675 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗(𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
147 | 145, 146 | nfeq 2762 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
148 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘𝑖 |
149 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘ℕ |
150 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) |
151 | 149, 150 | nfmpt 4674 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
152 | 148, 151 | nfeq 2762 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘 𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
153 | | fveq1 6102 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (𝑖‘𝑗) = ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗)) |
154 | 153 | coeq2d 5206 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))) |
155 | 154 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
156 | 155 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
157 | 152, 156 | ixpeq2d 38262 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
158 | 157 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
159 | 147, 158 | iuneq2df 38237 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
160 | 159 | sseq2d 3596 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))) |
161 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘 𝑗 ∈ ℕ |
162 | 152, 161 | nfan 1816 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑗 ∈ ℕ) |
163 | 155 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (vol‘(([,) ∘
(𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))) |
164 | 163 | a1d 25 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (𝑘 ∈ 𝑋 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))) |
165 | 164 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))) |
166 | 162, 165 | ralrimi 2940 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))) |
167 | 166 | prodeq2d 14491 |
. . . . . . . . . . . . 13
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))) |
168 | 147, 167 | mpteq2da 4671 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))) |
169 | 168 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))))) |
170 | 169 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) →
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))))) |
171 | 160, 170 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → ((𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))))))) |
172 | 171 | rspcev 3282 |
. . . . . . . 8
⊢ (((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
173 | 93, 144, 172 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
174 | 76, 173 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
175 | | eqeq1 2614 |
. . . . . . . . 9
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) → (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
176 | 175 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) → ((𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
177 | 176 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) → (∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
178 | 177 | elrab 3331 |
. . . . . 6
⊢
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ↔
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
179 | 174, 178 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
180 | | infxrlb 12036 |
. . . . 5
⊢ (({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆ ℝ* ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
181 | 74, 179, 180 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → inf({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
182 | 72, 181 | eqbrtrd 4605 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln*‘𝑋)‘𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
183 | 48, 50, 182 | syl2anc 691 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
184 | 47, 183 | pm2.61dan 828 |
1
⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |