Proof of Theorem ovnovollem1
| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {〈𝐴, (𝐹‘𝑗)〉} = {〈𝐴, (𝐹‘𝑗)〉}) |
| 2 | | ovnovollem1.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 3 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ 𝑉) |
| 4 | | ovnovollem1.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ)
↑m ℕ)) |
| 5 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
| 7 | 6 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ (ℝ ×
ℝ)) |
| 8 | | fsng 7157 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ (ℝ × ℝ)) →
({〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {〈𝐴, (𝐹‘𝑗)〉} = {〈𝐴, (𝐹‘𝑗)〉})) |
| 9 | 3, 7, 8 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {〈𝐴, (𝐹‘𝑗)〉} = {〈𝐴, (𝐹‘𝑗)〉})) |
| 10 | 1, 9 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶{(𝐹‘𝑗)}) |
| 11 | 7 | snssd 4809 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {(𝐹‘𝑗)} ⊆ (ℝ ×
ℝ)) |
| 12 | 10, 11 | fssd 6753 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶(ℝ ×
ℝ)) |
| 13 | | reex 11246 |
. . . . . . . 8
⊢ ℝ
∈ V |
| 14 | 13, 13 | xpex 7773 |
. . . . . . 7
⊢ (ℝ
× ℝ) ∈ V |
| 15 | 14 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℝ ×
ℝ) ∈ V) |
| 16 | | snex 5436 |
. . . . . . 7
⊢ {𝐴} ∈ V |
| 17 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝐴} ∈ V) |
| 18 | 15, 17 | elmapd 8880 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({〈𝐴, (𝐹‘𝑗)〉} ∈ ((ℝ × ℝ)
↑m {𝐴})
↔ {〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶(ℝ ×
ℝ))) |
| 19 | 12, 18 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {〈𝐴, (𝐹‘𝑗)〉} ∈ ((ℝ × ℝ)
↑m {𝐴})) |
| 20 | | ovnovollem1.i |
. . . 4
⊢ 𝐼 = (𝑗 ∈ ℕ ↦ {〈𝐴, (𝐹‘𝑗)〉}) |
| 21 | 19, 20 | fmptd 7134 |
. . 3
⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ)
↑m {𝐴})) |
| 22 | | ovexd 7466 |
. . . 4
⊢ (𝜑 → ((ℝ × ℝ)
↑m {𝐴})
∈ V) |
| 23 | | nnex 12272 |
. . . . 5
⊢ ℕ
∈ V |
| 24 | 23 | a1i 11 |
. . . 4
⊢ (𝜑 → ℕ ∈
V) |
| 25 | 22, 24 | elmapd 8880 |
. . 3
⊢ (𝜑 → (𝐼 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ) ↔ 𝐼:ℕ⟶((ℝ × ℝ)
↑m {𝐴}))) |
| 26 | 21, 25 | mpbird 257 |
. 2
⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ)) |
| 27 | | ovnovollem1.s |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
([,) ∘ 𝐹)) |
| 28 | | icof 45224 |
. . . . . . . . . . 11
⊢
[,):(ℝ* × ℝ*)⟶𝒫
ℝ* |
| 29 | 28 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → [,):(ℝ*
× ℝ*)⟶𝒫
ℝ*) |
| 30 | | rexpssxrxp 11306 |
. . . . . . . . . . 11
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ × ℝ)
⊆ (ℝ* × ℝ*)) |
| 32 | 29, 31, 6 | fcoss 45215 |
. . . . . . . . 9
⊢ (𝜑 → ([,) ∘ 𝐹):ℕ⟶𝒫
ℝ*) |
| 33 | 32 | ffnd 6737 |
. . . . . . . 8
⊢ (𝜑 → ([,) ∘ 𝐹) Fn ℕ) |
| 34 | | fniunfv 7267 |
. . . . . . . 8
⊢ (([,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,)
∘ 𝐹)) |
| 35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,)
∘ 𝐹)) |
| 36 | 35 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → ∪ ran ([,) ∘ 𝐹) = ∪
𝑗 ∈ ℕ (([,)
∘ 𝐹)‘𝑗)) |
| 37 | 27, 36 | sseqtrd 4020 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ ∪
𝑗 ∈ ℕ (([,)
∘ 𝐹)‘𝑗)) |
| 38 | | ovnovollem1.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
| 39 | | fvex 6919 |
. . . . . . . 8
⊢ (([,)
∘ 𝐹)‘𝑗) ∈ V |
| 40 | 23, 39 | iunex 7993 |
. . . . . . 7
⊢ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V |
| 41 | 40 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V) |
| 42 | 16 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝐴} ∈ V) |
| 43 | 2 | snn0d 4775 |
. . . . . 6
⊢ (𝜑 → {𝐴} ≠ ∅) |
| 44 | 38, 41, 42, 43 | mapss2 45210 |
. . . . 5
⊢ (𝜑 → (𝐵 ⊆ ∪
𝑗 ∈ ℕ (([,)
∘ 𝐹)‘𝑗) ↔ (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}))) |
| 45 | 37, 44 | mpbid 232 |
. . . 4
⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴})) |
| 46 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑗𝜑 |
| 47 | | fvexd 6921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘(𝐹‘𝑗)) ∈ V) |
| 48 | 46, 24, 47, 2 | iunmapsn 45222 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑m {𝐴}) = (∪
𝑗 ∈ ℕ
([,)‘(𝐹‘𝑗)) ↑m {𝐴})) |
| 49 | 48 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑m {𝐴}) = ∪
𝑗 ∈ ℕ
(([,)‘(𝐹‘𝑗)) ↑m {𝐴})) |
| 50 | | elmapfun 8906 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ((ℝ ×
ℝ) ↑m ℕ) → Fun 𝐹) |
| 51 | 4, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝐹) |
| 52 | 51 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun 𝐹) |
| 53 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
| 54 | 6 | fdmd 6746 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = ℕ) |
| 55 | 54 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝜑 → ℕ = dom 𝐹) |
| 56 | 55 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℕ = dom 𝐹) |
| 57 | 53, 56 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ dom 𝐹) |
| 58 | | fvco 7007 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑗 ∈ dom 𝐹) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗))) |
| 59 | 52, 57, 58 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗))) |
| 60 | 59 | iuneq2dv 5016 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ 𝑗 ∈ ℕ
([,)‘(𝐹‘𝑗))) |
| 61 | 60 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = (∪
𝑗 ∈ ℕ
([,)‘(𝐹‘𝑗)) ↑m {𝐴})) |
| 62 | 10 | ffund 6740 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun {〈𝐴, (𝐹‘𝑗)〉}) |
| 63 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) |
| 64 | | snex 5436 |
. . . . . . . . . . . . . . . 16
⊢
{〈𝐴, (𝐹‘𝑗)〉} ∈ V |
| 65 | 64 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ →
{〈𝐴, (𝐹‘𝑗)〉} ∈ V) |
| 66 | 20 | fvmpt2 7027 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℕ ∧
{〈𝐴, (𝐹‘𝑗)〉} ∈ V) → (𝐼‘𝑗) = {〈𝐴, (𝐹‘𝑗)〉}) |
| 67 | 63, 65, 66 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (𝐼‘𝑗) = {〈𝐴, (𝐹‘𝑗)〉}) |
| 68 | 67 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) = {〈𝐴, (𝐹‘𝑗)〉}) |
| 69 | 68 | funeqd 6588 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (Fun (𝐼‘𝑗) ↔ Fun {〈𝐴, (𝐹‘𝑗)〉})) |
| 70 | 62, 69 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun (𝐼‘𝑗)) |
| 71 | 70 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → Fun (𝐼‘𝑗)) |
| 72 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ {𝐴}) |
| 73 | 68 | dmeqd 5916 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = dom {〈𝐴, (𝐹‘𝑗)〉}) |
| 74 | 10 | fdmd 6746 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom {〈𝐴, (𝐹‘𝑗)〉} = {𝐴}) |
| 75 | 73, 74 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = {𝐴}) |
| 76 | 75 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴})) |
| 77 | 76 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴})) |
| 78 | 72, 77 | mpbird 257 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ dom (𝐼‘𝑗)) |
| 79 | | fvco 7007 |
. . . . . . . . . 10
⊢ ((Fun
(𝐼‘𝑗) ∧ 𝑘 ∈ dom (𝐼‘𝑗)) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘))) |
| 80 | 71, 78, 79 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘))) |
| 81 | 67 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → ((𝐼‘𝑗)‘𝑘) = ({〈𝐴, (𝐹‘𝑗)〉}‘𝑘)) |
| 82 | 81 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = ({〈𝐴, (𝐹‘𝑗)〉}‘𝑘)) |
| 83 | | elsni 4643 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝐴} → 𝑘 = 𝐴) |
| 84 | 83 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝐴} → ({〈𝐴, (𝐹‘𝑗)〉}‘𝑘) = ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴)) |
| 85 | 84 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({〈𝐴, (𝐹‘𝑗)〉}‘𝑘) = ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴)) |
| 86 | | fvexd 6921 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝑗) ∈ V) |
| 87 | | fvsng 7200 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ V) → ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴) = (𝐹‘𝑗)) |
| 88 | 2, 86, 87 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴) = (𝐹‘𝑗)) |
| 89 | 88 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴) = (𝐹‘𝑗)) |
| 90 | 82, 85, 89 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = (𝐹‘𝑗)) |
| 91 | 90 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘((𝐼‘𝑗)‘𝑘)) = ([,)‘(𝐹‘𝑗))) |
| 92 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘(𝐹‘𝑗)) = ([,)‘(𝐹‘𝑗))) |
| 93 | 80, 91, 92 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘(𝐹‘𝑗))) |
| 94 | 93 | ixpeq2dva 8952 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
{𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗))) |
| 95 | | fvex 6919 |
. . . . . . . . 9
⊢
([,)‘(𝐹‘𝑗)) ∈ V |
| 96 | 16, 95 | ixpconst 8947 |
. . . . . . . 8
⊢ X𝑘 ∈
{𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴}) |
| 97 | 96 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
{𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴})) |
| 98 | 94, 97 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
{𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,)‘(𝐹‘𝑗)) ↑m {𝐴})) |
| 99 | 98 | iuneq2dv 5016 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ
(([,)‘(𝐹‘𝑗)) ↑m {𝐴})) |
| 100 | 49, 61, 99 | 3eqtr4d 2787 |
. . . 4
⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑m {𝐴}) = ∪
𝑗 ∈ ℕ X𝑘 ∈
{𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
| 101 | 45, 100 | sseqtrd 4020 |
. . 3
⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
| 102 | | ovnovollem1.z |
. . . 4
⊢ (𝜑 → 𝑍 =
(Σ^‘((vol ∘ [,)) ∘ 𝐹))) |
| 103 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑗𝐹 |
| 104 | | ressxr 11305 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ* |
| 105 | | xpss2 5705 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ
× ℝ*)) |
| 106 | 104, 105 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℝ
× ℝ) ⊆ (ℝ × ℝ*) |
| 107 | 106 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (ℝ × ℝ)
⊆ (ℝ × ℝ*)) |
| 108 | 6, 107 | fssd 6753 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ*)) |
| 109 | 103, 108 | volicofmpt 46012 |
. . . . . 6
⊢ (𝜑 → ((vol ∘ [,)) ∘
𝐹) = (𝑗 ∈ ℕ ↦
(vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))))) |
| 110 | 67 | coeq2d 5873 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → ([,)
∘ (𝐼‘𝑗)) = ([,) ∘ {〈𝐴, (𝐹‘𝑗)〉})) |
| 111 | 110 | fveq1d 6908 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (([,)
∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {〈𝐴, (𝐹‘𝑗)〉})‘𝐴)) |
| 112 | 111 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {〈𝐴, (𝐹‘𝑗)〉})‘𝐴)) |
| 113 | | snidg 4660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
| 114 | 2, 113 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
| 115 | | dmsnopg 6233 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑗) ∈ V → dom {〈𝐴, (𝐹‘𝑗)〉} = {𝐴}) |
| 116 | 86, 115 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom {〈𝐴, (𝐹‘𝑗)〉} = {𝐴}) |
| 117 | 114, 116 | eleqtrrd 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ dom {〈𝐴, (𝐹‘𝑗)〉}) |
| 118 | 117 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ dom {〈𝐴, (𝐹‘𝑗)〉}) |
| 119 | | fvco 7007 |
. . . . . . . . . . . . . 14
⊢ ((Fun
{〈𝐴, (𝐹‘𝑗)〉} ∧ 𝐴 ∈ dom {〈𝐴, (𝐹‘𝑗)〉}) → (([,) ∘ {〈𝐴, (𝐹‘𝑗)〉})‘𝐴) = ([,)‘({〈𝐴, (𝐹‘𝑗)〉}‘𝐴))) |
| 120 | 62, 118, 119 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘
{〈𝐴, (𝐹‘𝑗)〉})‘𝐴) = ([,)‘({〈𝐴, (𝐹‘𝑗)〉}‘𝐴))) |
| 121 | | fvexd 6921 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ V) |
| 122 | 3, 121, 87 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴) = (𝐹‘𝑗)) |
| 123 | | 1st2nd2 8053 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) →
(𝐹‘𝑗) = 〈(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))〉) |
| 124 | 7, 123 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = 〈(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))〉) |
| 125 | 122, 124 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴) = 〈(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))〉) |
| 126 | 125 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
([,)‘({〈𝐴,
(𝐹‘𝑗)〉}‘𝐴)) = ([,)‘〈(1st
‘(𝐹‘𝑗)), (2nd
‘(𝐹‘𝑗))〉)) |
| 127 | | df-ov 7434 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))) = ([,)‘〈(1st
‘(𝐹‘𝑗)), (2nd
‘(𝐹‘𝑗))〉) |
| 128 | 127 | eqcomi 2746 |
. . . . . . . . . . . . . . 15
⊢
([,)‘〈(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))〉) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))) |
| 129 | 128 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
([,)‘〈(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))〉) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) |
| 130 | 126, 129 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
([,)‘({〈𝐴,
(𝐹‘𝑗)〉}‘𝐴)) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) |
| 131 | 112, 120,
130 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) |
| 132 | 131 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,)
∘ (𝐼‘𝑗))‘𝐴)) = (vol‘((1st
‘(𝐹‘𝑗))[,)(2nd
‘(𝐹‘𝑗))))) |
| 133 | | xp1st 8046 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘𝑗)) ∈ ℝ) |
| 134 | 7, 133 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1st
‘(𝐹‘𝑗)) ∈
ℝ) |
| 135 | | xp2nd 8047 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘𝑗)) ∈ ℝ) |
| 136 | 7, 135 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2nd
‘(𝐹‘𝑗)) ∈
ℝ) |
| 137 | | volicore 46596 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑗)) ∈ ℝ) →
(vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ) |
| 138 | 134, 136,
137 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ) |
| 139 | 132, 138 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,)
∘ (𝐼‘𝑗))‘𝐴)) ∈ ℝ) |
| 140 | 139 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,)
∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ) |
| 141 | | 2fveq3 6911 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐴 → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴))) |
| 142 | 141 | prodsn 15998 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴))) |
| 143 | 3, 140, 142 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴))) |
| 144 | 143, 132 | eqtr2d 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
| 145 | 144 | mpteq2dva 5242 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ℕ ↦
(vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))) |
| 146 | 109, 145 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ((vol ∘ [,)) ∘
𝐹) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))) |
| 147 | 146 | fveq2d 6910 |
. . . 4
⊢ (𝜑 →
(Σ^‘((vol ∘ [,)) ∘ 𝐹)) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) |
| 148 | 102, 147 | eqtrd 2777 |
. . 3
⊢ (𝜑 → 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) |
| 149 | 101, 148 | jca 511 |
. 2
⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) |
| 150 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → (𝑖‘𝑗) = (𝐼‘𝑗)) |
| 151 | 150 | coeq2d 5873 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗))) |
| 152 | 151 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
| 153 | 152 | ixpeq2dv 8953 |
. . . . . 6
⊢ (𝑖 = 𝐼 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
| 154 | 153 | iuneq2d 5022 |
. . . . 5
⊢ (𝑖 = 𝐼 → ∪
𝑗 ∈ ℕ X𝑘 ∈
{𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
{𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
| 155 | 154 | sseq2d 4016 |
. . . 4
⊢ (𝑖 = 𝐼 → ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))) |
| 156 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → 𝑖 = 𝐼) |
| 157 | 156 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (𝑖‘𝑗) = (𝐼‘𝑗)) |
| 158 | 157 | coeq2d 5873 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗))) |
| 159 | 158 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
| 160 | 159 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
| 161 | 160 | prodeq2dv 15958 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
| 162 | 161 | mpteq2dv 5244 |
. . . . . 6
⊢ (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))) |
| 163 | 162 | fveq2d 6910 |
. . . . 5
⊢ (𝑖 = 𝐼 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) |
| 164 | 163 | eqeq2d 2748 |
. . . 4
⊢ (𝑖 = 𝐼 → (𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) |
| 165 | 155, 164 | anbi12d 632 |
. . 3
⊢ (𝑖 = 𝐼 → (((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))) |
| 166 | 165 | rspcev 3622 |
. 2
⊢ ((𝐼 ∈ (((ℝ ×
ℝ) ↑m {𝐴}) ↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
| 167 | 26, 149, 166 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |