Proof of Theorem ovnovollem1
Step | Hyp | Ref
| Expression |
1 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {〈𝐴, (𝐹‘𝑗)〉} = {〈𝐴, (𝐹‘𝑗)〉}) |
2 | | ovnovollem1.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ 𝑉) |
4 | | ovnovollem1.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) |
5 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
7 | 6 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ (ℝ ×
ℝ)) |
8 | | fsng 6310 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ (ℝ × ℝ)) →
({〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {〈𝐴, (𝐹‘𝑗)〉} = {〈𝐴, (𝐹‘𝑗)〉})) |
9 | 3, 7, 8 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶{(𝐹‘𝑗)} ↔ {〈𝐴, (𝐹‘𝑗)〉} = {〈𝐴, (𝐹‘𝑗)〉})) |
10 | 1, 9 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶{(𝐹‘𝑗)}) |
11 | 7 | snssd 4281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {(𝐹‘𝑗)} ⊆ (ℝ ×
ℝ)) |
12 | 10, 11 | fssd 5970 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶(ℝ ×
ℝ)) |
13 | | reex 9906 |
. . . . . . . 8
⊢ ℝ
∈ V |
14 | 13, 13 | xpex 6860 |
. . . . . . 7
⊢ (ℝ
× ℝ) ∈ V |
15 | 14 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (ℝ ×
ℝ) ∈ V) |
16 | | snex 4835 |
. . . . . . 7
⊢ {𝐴} ∈ V |
17 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {𝐴} ∈ V) |
18 | 15, 17 | elmapd 7758 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({〈𝐴, (𝐹‘𝑗)〉} ∈ ((ℝ × ℝ)
↑𝑚 {𝐴}) ↔ {〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶(ℝ ×
ℝ))) |
19 | 12, 18 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → {〈𝐴, (𝐹‘𝑗)〉} ∈ ((ℝ × ℝ)
↑𝑚 {𝐴})) |
20 | | ovnovollem1.i |
. . . 4
⊢ 𝐼 = (𝑗 ∈ ℕ ↦ {〈𝐴, (𝐹‘𝑗)〉}) |
21 | 19, 20 | fmptd 6292 |
. . 3
⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ)
↑𝑚 {𝐴})) |
22 | | ovex 6577 |
. . . . 5
⊢ ((ℝ
× ℝ) ↑𝑚 {𝐴}) ∈ V |
23 | 22 | a1i 11 |
. . . 4
⊢ (𝜑 → ((ℝ × ℝ)
↑𝑚 {𝐴}) ∈ V) |
24 | | nnex 10903 |
. . . . 5
⊢ ℕ
∈ V |
25 | 24 | a1i 11 |
. . . 4
⊢ (𝜑 → ℕ ∈
V) |
26 | 23, 25 | elmapd 7758 |
. . 3
⊢ (𝜑 → (𝐼 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚 ℕ)
↔ 𝐼:ℕ⟶((ℝ × ℝ)
↑𝑚 {𝐴}))) |
27 | 21, 26 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚
ℕ)) |
28 | | ovnovollem1.s |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
([,) ∘ 𝐹)) |
29 | | icof 38406 |
. . . . . . . . . . 11
⊢
[,):(ℝ* × ℝ*)⟶𝒫
ℝ* |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → [,):(ℝ*
× ℝ*)⟶𝒫
ℝ*) |
31 | | rexpssxrxp 9963 |
. . . . . . . . . . 11
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
32 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ × ℝ)
⊆ (ℝ* × ℝ*)) |
33 | 30, 32, 6 | fcoss 38397 |
. . . . . . . . 9
⊢ (𝜑 → ([,) ∘ 𝐹):ℕ⟶𝒫
ℝ*) |
34 | 33 | ffnd 5959 |
. . . . . . . 8
⊢ (𝜑 → ([,) ∘ 𝐹) Fn ℕ) |
35 | | fniunfv 6409 |
. . . . . . . 8
⊢ (([,)
∘ 𝐹) Fn ℕ
→ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,)
∘ 𝐹)) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ ran ([,)
∘ 𝐹)) |
37 | 36 | eqcomd 2616 |
. . . . . 6
⊢ (𝜑 → ∪ ran ([,) ∘ 𝐹) = ∪
𝑗 ∈ ℕ (([,)
∘ 𝐹)‘𝑗)) |
38 | 28, 37 | sseqtrd 3604 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ ∪
𝑗 ∈ ℕ (([,)
∘ 𝐹)‘𝑗)) |
39 | | ovnovollem1.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
40 | | fvex 6113 |
. . . . . . . 8
⊢ (([,)
∘ 𝐹)‘𝑗) ∈ V |
41 | 24, 40 | iunex 7039 |
. . . . . . 7
⊢ ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V |
42 | 41 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V) |
43 | 16 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝐴} ∈ V) |
44 | 2 | snn0d 38284 |
. . . . . 6
⊢ (𝜑 → {𝐴} ≠ ∅) |
45 | 39, 42, 43, 44 | mapss2 38392 |
. . . . 5
⊢ (𝜑 → (𝐵 ⊆ ∪
𝑗 ∈ ℕ (([,)
∘ 𝐹)‘𝑗) ↔ (𝐵 ↑𝑚 {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑𝑚 {𝐴}))) |
46 | 38, 45 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝐵 ↑𝑚 {𝐴}) ⊆ (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑𝑚 {𝐴})) |
47 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑗𝜑 |
48 | | fvex 6113 |
. . . . . . . 8
⊢
([,)‘(𝐹‘𝑗)) ∈ V |
49 | 48 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ([,)‘(𝐹‘𝑗)) ∈ V) |
50 | 47, 25, 49, 2 | iunmapsn 38404 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑𝑚 {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑𝑚 {𝐴})) |
51 | 50 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑𝑚 {𝐴}) = ∪ 𝑗 ∈ ℕ (([,)‘(𝐹‘𝑗)) ↑𝑚 {𝐴})) |
52 | | elmapfun 7767 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ((ℝ ×
ℝ) ↑𝑚 ℕ) → Fun 𝐹) |
53 | 4, 52 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝐹) |
54 | 53 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun 𝐹) |
55 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
56 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:ℕ⟶(ℝ ×
ℝ) → dom 𝐹 =
ℕ) |
57 | 6, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = ℕ) |
58 | 57 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝜑 → ℕ = dom 𝐹) |
59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ℕ = dom 𝐹) |
60 | 55, 59 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ dom 𝐹) |
61 | | fvco 6184 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑗 ∈ dom 𝐹) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗))) |
62 | 54, 60, 61 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹‘𝑗))) |
63 | 62 | iuneq2dv 4478 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ∪ 𝑗 ∈ ℕ
([,)‘(𝐹‘𝑗))) |
64 | 63 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑𝑚 {𝐴}) = (∪ 𝑗 ∈ ℕ ([,)‘(𝐹‘𝑗)) ↑𝑚 {𝐴})) |
65 | | ffun 5961 |
. . . . . . . . . . . . 13
⊢
({〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶{(𝐹‘𝑗)} → Fun {〈𝐴, (𝐹‘𝑗)〉}) |
66 | 10, 65 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun {〈𝐴, (𝐹‘𝑗)〉}) |
67 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) |
68 | | snex 4835 |
. . . . . . . . . . . . . . . 16
⊢
{〈𝐴, (𝐹‘𝑗)〉} ∈ V |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ →
{〈𝐴, (𝐹‘𝑗)〉} ∈ V) |
70 | 20 | fvmpt2 6200 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℕ ∧
{〈𝐴, (𝐹‘𝑗)〉} ∈ V) → (𝐼‘𝑗) = {〈𝐴, (𝐹‘𝑗)〉}) |
71 | 67, 69, 70 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (𝐼‘𝑗) = {〈𝐴, (𝐹‘𝑗)〉}) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑗) = {〈𝐴, (𝐹‘𝑗)〉}) |
73 | 72 | funeqd 5825 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (Fun (𝐼‘𝑗) ↔ Fun {〈𝐴, (𝐹‘𝑗)〉})) |
74 | 66, 73 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → Fun (𝐼‘𝑗)) |
75 | 74 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → Fun (𝐼‘𝑗)) |
76 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ {𝐴}) |
77 | 72 | dmeqd 5248 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = dom {〈𝐴, (𝐹‘𝑗)〉}) |
78 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢
({〈𝐴, (𝐹‘𝑗)〉}:{𝐴}⟶(ℝ × ℝ) →
dom {〈𝐴, (𝐹‘𝑗)〉} = {𝐴}) |
79 | 12, 78 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom {〈𝐴, (𝐹‘𝑗)〉} = {𝐴}) |
80 | 77, 79 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → dom (𝐼‘𝑗) = {𝐴}) |
81 | 80 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴})) |
82 | 81 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (𝑘 ∈ dom (𝐼‘𝑗) ↔ 𝑘 ∈ {𝐴})) |
83 | 76, 82 | mpbird 246 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ dom (𝐼‘𝑗)) |
84 | | fvco 6184 |
. . . . . . . . . 10
⊢ ((Fun
(𝐼‘𝑗) ∧ 𝑘 ∈ dom (𝐼‘𝑗)) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘))) |
85 | 75, 83, 84 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘((𝐼‘𝑗)‘𝑘))) |
86 | 71 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → ((𝐼‘𝑗)‘𝑘) = ({〈𝐴, (𝐹‘𝑗)〉}‘𝑘)) |
87 | 86 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = ({〈𝐴, (𝐹‘𝑗)〉}‘𝑘)) |
88 | | elsni 4142 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝐴} → 𝑘 = 𝐴) |
89 | 88 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝐴} → ({〈𝐴, (𝐹‘𝑗)〉}‘𝑘) = ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴)) |
90 | 89 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({〈𝐴, (𝐹‘𝑗)〉}‘𝑘) = ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴)) |
91 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘𝑗) ∈ V |
92 | 91 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝑗) ∈ V) |
93 | | fvsng 6352 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝑗) ∈ V) → ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴) = (𝐹‘𝑗)) |
94 | 2, 92, 93 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴) = (𝐹‘𝑗)) |
95 | 94 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴) = (𝐹‘𝑗)) |
96 | 87, 90, 95 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼‘𝑗)‘𝑘) = (𝐹‘𝑗)) |
97 | 96 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘((𝐼‘𝑗)‘𝑘)) = ([,)‘(𝐹‘𝑗))) |
98 | | eqidd 2611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘(𝐹‘𝑗)) = ([,)‘(𝐹‘𝑗))) |
99 | 85, 97, 98 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼‘𝑗))‘𝑘) = ([,)‘(𝐹‘𝑗))) |
100 | 99 | ixpeq2dva 7809 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
{𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} ([,)‘(𝐹‘𝑗))) |
101 | 16, 48 | ixpconst 7804 |
. . . . . . . 8
⊢ X𝑘 ∈
{𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑𝑚 {𝐴}) |
102 | 101 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
{𝐴} ([,)‘(𝐹‘𝑗)) = (([,)‘(𝐹‘𝑗)) ↑𝑚 {𝐴})) |
103 | 100, 102 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
{𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,)‘(𝐹‘𝑗)) ↑𝑚 {𝐴})) |
104 | 103 | iuneq2dv 4478 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ
(([,)‘(𝐹‘𝑗)) ↑𝑚
{𝐴})) |
105 | 51, 64, 104 | 3eqtr4d 2654 |
. . . 4
⊢ (𝜑 → (∪ 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑𝑚 {𝐴}) = ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
106 | 46, 105 | sseqtrd 3604 |
. . 3
⊢ (𝜑 → (𝐵 ↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
107 | | ovnovollem1.z |
. . . 4
⊢ (𝜑 → 𝑍 =
(Σ^‘((vol ∘ [,)) ∘ 𝐹))) |
108 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑗𝐹 |
109 | | ressxr 9962 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ* |
110 | | xpss2 5152 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ
× ℝ*)) |
111 | 109, 110 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℝ
× ℝ) ⊆ (ℝ × ℝ*) |
112 | 111 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (ℝ × ℝ)
⊆ (ℝ × ℝ*)) |
113 | 6, 112 | fssd 5970 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ*)) |
114 | 108, 113 | volicofmpt 38890 |
. . . . . 6
⊢ (𝜑 → ((vol ∘ [,)) ∘
𝐹) = (𝑗 ∈ ℕ ↦
(vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))))) |
115 | 71 | coeq2d 5206 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → ([,)
∘ (𝐼‘𝑗)) = ([,) ∘ {〈𝐴, (𝐹‘𝑗)〉})) |
116 | 115 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → (([,)
∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {〈𝐴, (𝐹‘𝑗)〉})‘𝐴)) |
117 | 116 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = (([,) ∘ {〈𝐴, (𝐹‘𝑗)〉})‘𝐴)) |
118 | | snidg 4153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
119 | 2, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
120 | | dmsnopg 5524 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑗) ∈ V → dom {〈𝐴, (𝐹‘𝑗)〉} = {𝐴}) |
121 | 92, 120 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom {〈𝐴, (𝐹‘𝑗)〉} = {𝐴}) |
122 | 119, 121 | eleqtrrd 2691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ dom {〈𝐴, (𝐹‘𝑗)〉}) |
123 | 122 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ dom {〈𝐴, (𝐹‘𝑗)〉}) |
124 | | fvco 6184 |
. . . . . . . . . . . . . 14
⊢ ((Fun
{〈𝐴, (𝐹‘𝑗)〉} ∧ 𝐴 ∈ dom {〈𝐴, (𝐹‘𝑗)〉}) → (([,) ∘ {〈𝐴, (𝐹‘𝑗)〉})‘𝐴) = ([,)‘({〈𝐴, (𝐹‘𝑗)〉}‘𝐴))) |
125 | 66, 123, 124 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘
{〈𝐴, (𝐹‘𝑗)〉})‘𝐴) = ([,)‘({〈𝐴, (𝐹‘𝑗)〉}‘𝐴))) |
126 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ V) |
127 | 3, 126, 93 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴) = (𝐹‘𝑗)) |
128 | | 1st2nd2 7096 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) →
(𝐹‘𝑗) = 〈(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))〉) |
129 | 7, 128 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = 〈(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))〉) |
130 | 127, 129 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ({〈𝐴, (𝐹‘𝑗)〉}‘𝐴) = 〈(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))〉) |
131 | 130 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
([,)‘({〈𝐴,
(𝐹‘𝑗)〉}‘𝐴)) = ([,)‘〈(1st
‘(𝐹‘𝑗)), (2nd
‘(𝐹‘𝑗))〉)) |
132 | | df-ov 6552 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))) = ([,)‘〈(1st
‘(𝐹‘𝑗)), (2nd
‘(𝐹‘𝑗))〉) |
133 | 132 | eqcomi 2619 |
. . . . . . . . . . . . . . 15
⊢
([,)‘〈(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))〉) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))) |
134 | 133 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
([,)‘〈(1st ‘(𝐹‘𝑗)), (2nd ‘(𝐹‘𝑗))〉) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) |
135 | 131, 134 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
([,)‘({〈𝐴,
(𝐹‘𝑗)〉}‘𝐴)) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) |
136 | 117, 125,
135 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (([,) ∘ (𝐼‘𝑗))‘𝐴) = ((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) |
137 | 136 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,)
∘ (𝐼‘𝑗))‘𝐴)) = (vol‘((1st
‘(𝐹‘𝑗))[,)(2nd
‘(𝐹‘𝑗))))) |
138 | | xp1st 7089 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘𝑗)) ∈ ℝ) |
139 | 7, 138 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (1st
‘(𝐹‘𝑗)) ∈
ℝ) |
140 | | xp2nd 7090 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑗) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘𝑗)) ∈ ℝ) |
141 | 7, 140 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2nd
‘(𝐹‘𝑗)) ∈
ℝ) |
142 | | volicore 39471 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝐹‘𝑗)) ∈ ℝ ∧ (2nd
‘(𝐹‘𝑗)) ∈ ℝ) →
(vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ) |
143 | 139, 141,
142 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) ∈ ℝ) |
144 | 137, 143 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,)
∘ (𝐼‘𝑗))‘𝐴)) ∈ ℝ) |
145 | 144 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘(([,)
∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ) |
146 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐴 → (([,) ∘ (𝐼‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝐴)) |
147 | 146 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐴 → (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴))) |
148 | 147 | prodsn 14531 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴)) ∈ ℂ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴))) |
149 | 3, 145, 148 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝐴))) |
150 | 149, 137 | eqtr2d 2645 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗)))) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
151 | 150 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ℕ ↦
(vol‘((1st ‘(𝐹‘𝑗))[,)(2nd ‘(𝐹‘𝑗))))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))) |
152 | 114, 151 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → ((vol ∘ [,)) ∘
𝐹) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))) |
153 | 152 | fveq2d 6107 |
. . . 4
⊢ (𝜑 →
(Σ^‘((vol ∘ [,)) ∘ 𝐹)) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) |
154 | 107, 153 | eqtrd 2644 |
. . 3
⊢ (𝜑 → 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) |
155 | 106, 154 | jca 553 |
. 2
⊢ (𝜑 → ((𝐵 ↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) |
156 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → (𝑖‘𝑗) = (𝐼‘𝑗)) |
157 | 156 | coeq2d 5206 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗))) |
158 | 157 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
159 | 158 | ixpeq2dv 7810 |
. . . . . 6
⊢ (𝑖 = 𝐼 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
160 | 159 | iuneq2d 4483 |
. . . . 5
⊢ (𝑖 = 𝐼 → ∪
𝑗 ∈ ℕ X𝑘 ∈
{𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
{𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
161 | 160 | sseq2d 3596 |
. . . 4
⊢ (𝑖 = 𝐼 → ((𝐵 ↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ (𝐵 ↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘))) |
162 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → 𝑖 = 𝐼) |
163 | 162 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (𝑖‘𝑗) = (𝐼‘𝑗)) |
164 | 163 | coeq2d 5206 |
. . . . . . . . . 10
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝐼‘𝑗))) |
165 | 164 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝐼‘𝑗))‘𝑘)) |
166 | 165 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑘 ∈ {𝐴}) → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
167 | 166 | prodeq2dv 14492 |
. . . . . . 7
⊢ (𝑖 = 𝐼 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))) |
168 | 167 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))) |
169 | 168 | fveq2d 6107 |
. . . . 5
⊢ (𝑖 = 𝐼 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) |
170 | 169 | eqeq2d 2620 |
. . . 4
⊢ (𝑖 = 𝐼 → (𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) |
171 | 161, 170 | anbi12d 743 |
. . 3
⊢ (𝑖 = 𝐼 → (((𝐵 ↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ((𝐵 ↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))))) |
172 | 171 | rspcev 3282 |
. 2
⊢ ((𝐼 ∈ (((ℝ ×
ℝ) ↑𝑚 {𝐴}) ↑𝑚 ℕ) ∧
((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
173 | 27, 155, 172 | syl2anc 691 |
1
⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |