| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . 6
⊢ (𝑋 = ∅ →
(voln*‘𝑋) =
(voln*‘∅)) |
| 2 | 1 | fveq1d 6908 |
. . . . 5
⊢ (𝑋 = ∅ →
((voln*‘𝑋)‘𝐴) = ((voln*‘∅)‘𝐴)) |
| 3 | 2 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐴) = ((voln*‘∅)‘𝐴)) |
| 4 | | ovnlecvr2.s |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
| 5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
| 6 | | 1nn 12277 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
| 7 | | ne0i 4341 |
. . . . . . . . . . 11
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
| 8 | 6, 7 | ax-mp 5 |
. . . . . . . . . 10
⊢ ℕ
≠ ∅ |
| 9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℕ ≠
∅) |
| 10 | | iunconst 5001 |
. . . . . . . . 9
⊢ (ℕ
≠ ∅ → ∪ 𝑗 ∈ ℕ {∅} =
{∅}) |
| 11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ {∅} =
{∅}) |
| 12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∪ 𝑗 ∈ ℕ {∅} =
{∅}) |
| 13 | | ixpeq1 8948 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ ∅ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
| 14 | | ixp0x 8966 |
. . . . . . . . . . . 12
⊢ X𝑘 ∈
∅ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = {∅} |
| 15 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → X𝑘 ∈
∅ (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = {∅}) |
| 16 | 13, 15 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = {∅}) |
| 17 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 = ∅ ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = {∅}) |
| 18 | 17 | iuneq2dv 5016 |
. . . . . . . 8
⊢ (𝑋 = ∅ → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪
𝑗 ∈ ℕ
{∅}) |
| 19 | 18 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪
𝑗 ∈ ℕ
{∅}) |
| 20 | | reex 11246 |
. . . . . . . . 9
⊢ ℝ
∈ V |
| 21 | | mapdm0 8882 |
. . . . . . . . 9
⊢ (ℝ
∈ V → (ℝ ↑m ∅) =
{∅}) |
| 22 | 20, 21 | ax-mp 5 |
. . . . . . . 8
⊢ (ℝ
↑m ∅) = {∅} |
| 23 | 22 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → (ℝ
↑m ∅) = {∅}) |
| 24 | 12, 19, 23 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (ℝ ↑m
∅)) |
| 25 | 5, 24 | sseqtrd 4020 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴 ⊆ (ℝ ↑m
∅)) |
| 26 | 25 | ovn0val 46565 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) →
((voln*‘∅)‘𝐴) = 0) |
| 27 | 3, 26 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐴) = 0) |
| 28 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑗𝜑 |
| 29 | | nnex 12272 |
. . . . . 6
⊢ ℕ
∈ V |
| 30 | 29 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℕ ∈
V) |
| 31 | | icossicc 13476 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
| 32 | | ovnlecvr2.l |
. . . . . . 7
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
| 33 | | ovnlecvr2.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 34 | 33 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin) |
| 35 | | ovnlecvr2.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m
𝑋)) |
| 36 | 35 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑m 𝑋)) |
| 37 | | elmapi 8889 |
. . . . . . . 8
⊢ ((𝐶‘𝑗) ∈ (ℝ ↑m 𝑋) → (𝐶‘𝑗):𝑋⟶ℝ) |
| 38 | 36, 37 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ) |
| 39 | | ovnlecvr2.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m
𝑋)) |
| 40 | 39 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑m 𝑋)) |
| 41 | | elmapi 8889 |
. . . . . . . 8
⊢ ((𝐷‘𝑗) ∈ (ℝ ↑m 𝑋) → (𝐷‘𝑗):𝑋⟶ℝ) |
| 42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) |
| 43 | 32, 34, 38, 42 | hoidmvcl 46597 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,)+∞)) |
| 44 | 31, 43 | sselid 3981 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) ∈ (0[,]+∞)) |
| 45 | 28, 30, 44 | sge0ge0mpt 46453 |
. . . 4
⊢ (𝜑 → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
| 46 | 45 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
| 47 | 27, 46 | eqbrtrd 5165 |
. 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
| 48 | | simpl 482 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝜑) |
| 49 | | neqne 2948 |
. . . 4
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
| 50 | 49 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
| 51 | 33 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ∈ Fin) |
| 52 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ≠ ∅) |
| 53 | 38 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑗)‘𝑘) ∈ ℝ) |
| 54 | 42 | ffvelcdmda 7104 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈ ℝ) |
| 55 | 54 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐷‘𝑗)‘𝑘) ∈
ℝ*) |
| 56 | | icossre 13468 |
. . . . . . . . . . . . 13
⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ*) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ) |
| 57 | 53, 55, 56 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ) |
| 58 | 57 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ) |
| 59 | | ss2ixp 8950 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ ℝ → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ℝ) |
| 60 | 58, 59 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ℝ) |
| 61 | 20 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈
V) |
| 62 | | ixpconstg 8946 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ Fin ∧ ℝ ∈
V) → X𝑘 ∈ 𝑋 ℝ = (ℝ ↑m 𝑋)) |
| 63 | 33, 61, 62 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → X𝑘 ∈
𝑋 ℝ = (ℝ
↑m 𝑋)) |
| 64 | 63 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 ℝ = (ℝ
↑m 𝑋)) |
| 65 | 60, 64 | sseqtrd 4020 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ (ℝ ↑m 𝑋)) |
| 66 | 65 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ (ℝ ↑m 𝑋)) |
| 67 | | iunss 5045 |
. . . . . . . 8
⊢ (∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ (ℝ ↑m 𝑋) ↔ ∀𝑗 ∈ ℕ X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ (ℝ ↑m 𝑋)) |
| 68 | 66, 67 | sylibr 234 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) ⊆ (ℝ ↑m 𝑋)) |
| 69 | 4, 68 | sstrd 3994 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) |
| 70 | 69 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐴 ⊆ (ℝ ↑m 𝑋)) |
| 71 | | eqid 2737 |
. . . . 5
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
| 72 | 51, 52, 70, 71 | ovnn0val 46566 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln*‘𝑋)‘𝐴) = inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
)) |
| 73 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆
ℝ* |
| 74 | 73 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆
ℝ*) |
| 75 | 28, 30, 44 | sge0xrclmpt 46443 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈
ℝ*) |
| 76 | 75 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈
ℝ*) |
| 77 | | opelxpi 5722 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶‘𝑗)‘𝑘) ∈ ℝ ∧ ((𝐷‘𝑗)‘𝑘) ∈ ℝ) → 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉 ∈ (ℝ ×
ℝ)) |
| 78 | 53, 54, 77 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉 ∈ (ℝ ×
ℝ)) |
| 79 | 78 | fmpttd 7135 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉):𝑋⟶(ℝ ×
ℝ)) |
| 80 | 20, 20 | xpex 7773 |
. . . . . . . . . . . . . 14
⊢ (ℝ
× ℝ) ∈ V |
| 81 | 80 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℝ ×
ℝ) ∈ V) |
| 82 | | elmapg 8879 |
. . . . . . . . . . . . 13
⊢
(((ℝ × ℝ) ∈ V ∧ 𝑋 ∈ Fin) → ((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ ((ℝ × ℝ)
↑m 𝑋)
↔ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉):𝑋⟶(ℝ ×
ℝ))) |
| 83 | 81, 34, 82 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ ((ℝ × ℝ)
↑m 𝑋)
↔ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉):𝑋⟶(ℝ ×
ℝ))) |
| 84 | 79, 83 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ ((ℝ × ℝ)
↑m 𝑋)) |
| 85 | 84 | fmpttd 7135 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)):ℕ⟶((ℝ ×
ℝ) ↑m 𝑋)) |
| 86 | | ovexd 7466 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℝ × ℝ)
↑m 𝑋)
∈ V) |
| 87 | | elmapg 8879 |
. . . . . . . . . . 11
⊢
((((ℝ × ℝ) ↑m 𝑋) ∈ V ∧ ℕ ∈ V) →
((𝑗 ∈ ℕ ↦
(𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ↔ (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)):ℕ⟶((ℝ ×
ℝ) ↑m 𝑋))) |
| 88 | 86, 30, 87 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ↔ (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)):ℕ⟶((ℝ ×
ℝ) ↑m 𝑋))) |
| 89 | 85, 88 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) |
| 90 | 89 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) |
| 91 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
| 92 | | mptexg 7241 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑋 ∈ Fin → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ V) |
| 93 | 33, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ V) |
| 94 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ V) |
| 95 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
| 96 | 95 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ ∧ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) ∈ V) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗) = (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
| 97 | 91, 94, 96 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗) = (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
| 98 | 97 | coeq2d 5873 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗)) = ([,) ∘ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))) |
| 99 | 98 | fveq1d 6908 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) = (([,) ∘ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑘)) |
| 100 | 99 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) = (([,) ∘ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑘)) |
| 101 | 79 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉):𝑋⟶(ℝ ×
ℝ)) |
| 102 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
| 103 | 101, 102 | fvovco 45198 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑘) = ((1st ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘))[,)(2nd ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘)))) |
| 104 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
| 105 | | opex 5469 |
. . . . . . . . . . . . . . . . . . . 20
⊢
〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉 ∈ V |
| 106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉 ∈ V) |
| 107 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) |
| 108 | 107 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ 𝑋 ∧ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉 ∈ V) → ((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘) = 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) |
| 109 | 104, 106,
108 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘) = 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) |
| 110 | 109 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘)) = (1st ‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
| 111 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶‘𝑗)‘𝑘) ∈ V |
| 112 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷‘𝑗)‘𝑘) ∈ V |
| 113 | | op1stg 8026 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐶‘𝑗)‘𝑘) ∈ V ∧ ((𝐷‘𝑗)‘𝑘) ∈ V) → (1st
‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = ((𝐶‘𝑗)‘𝑘)) |
| 114 | 111, 112,
113 | mp2an 692 |
. . . . . . . . . . . . . . . . . 18
⊢
(1st ‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = ((𝐶‘𝑗)‘𝑘) |
| 115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1st
‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = ((𝐶‘𝑗)‘𝑘)) |
| 116 | 110, 115 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘)) = ((𝐶‘𝑗)‘𝑘)) |
| 117 | 109 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘)) = (2nd ‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
| 118 | 111, 112 | op2nd 8023 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = ((𝐷‘𝑗)‘𝑘) |
| 119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (2nd
‘〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) = ((𝐷‘𝑗)‘𝑘)) |
| 120 | 117, 119 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘)) = ((𝐷‘𝑗)‘𝑘)) |
| 121 | 116, 120 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((1st ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘))[,)(2nd ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘))) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
| 122 | 121 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((1st ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘))[,)(2nd ‘((𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)‘𝑘))) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
| 123 | 100, 103,
122 | 3eqtrrd 2782 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
| 124 | 123 | ixpeq2dva 8952 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
| 125 | 124 | iuneq2dv 5016 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)) = ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
| 126 | 4, 125 | sseqtrd 4020 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
| 127 | 126 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
| 128 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))) |
| 129 | 51 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin) |
| 130 | 52 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ ℕ) → 𝑋 ≠ ∅) |
| 131 | 38 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑋⟶ℝ) |
| 132 | 42 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑋⟶ℝ) |
| 133 | 32, 129, 130, 131, 132 | hoidmvn0val 46599 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
| 134 | 133 | mpteq2dva 5242 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) |
| 135 | 134 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))) |
| 136 | 123 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
| 137 | 136 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
| 138 | 137 | prodeq2dv 15958 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
| 139 | 138 | mpteq2dva 5242 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) |
| 140 | 139 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))) |
| 141 | 140 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))))) |
| 142 | 128, 135,
141 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))))) |
| 143 | 127, 142 | jca 511 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))))) |
| 144 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝑖 |
| 145 | | nfmpt1 5250 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗(𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
| 146 | 144, 145 | nfeq 2919 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
| 147 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘𝑖 |
| 148 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘ℕ |
| 149 | | nfmpt1 5250 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉) |
| 150 | 148, 149 | nfmpt 5249 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
| 151 | 147, 150 | nfeq 2919 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘 𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) |
| 152 | | fveq1 6905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (𝑖‘𝑗) = ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗)) |
| 153 | 152 | coeq2d 5873 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))) |
| 154 | 153 | fveq1d 6908 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
| 155 | 154 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
| 156 | 151, 155 | ixpeq2d 45073 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
| 157 | 156 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
| 158 | 146, 157 | iuneq2df 45052 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)) |
| 159 | 158 | sseq2d 4016 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))) |
| 160 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘 𝑗 ∈ ℕ |
| 161 | 151, 160 | nfan 1899 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑗 ∈ ℕ) |
| 162 | 154 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (vol‘(([,) ∘
(𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))) |
| 163 | 162 | a1d 25 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (𝑘 ∈ 𝑋 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))) |
| 164 | 163 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))) |
| 165 | 161, 164 | ralrimi 3257 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))) |
| 166 | 165 | prodeq2d 15957 |
. . . . . . . . . . . . 13
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))) |
| 167 | 146, 166 | mpteq2da 5240 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))) |
| 168 | 167 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))))) |
| 169 | 168 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) →
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))))) |
| 170 | 159, 169 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) → ((𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘))))))) |
| 171 | 170 | rspcev 3622 |
. . . . . . . 8
⊢ (((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉)) ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈((𝐶‘𝑗)‘𝑘), ((𝐷‘𝑗)‘𝑘)〉))‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
| 172 | 90, 143, 171 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∃𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
| 173 | 76, 172 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
| 174 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) → (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
| 175 | 174 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) → ((𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
| 176 | 175 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) → (∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
| 177 | 176 | elrab 3692 |
. . . . . 6
⊢
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ↔
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
| 178 | 173, 177 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
| 179 | | infxrlb 13376 |
. . . . 5
⊢ (({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆ ℝ* ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗)))) ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
| 180 | 74, 178, 179 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → inf({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
| 181 | 72, 180 | eqbrtrd 5165 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln*‘𝑋)‘𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
| 182 | 48, 50, 181 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln*‘𝑋)‘𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
| 183 | 47, 182 | pm2.61dan 813 |
1
⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |