Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ovnovollem1 Structured version   Visualization version   GIF version

Theorem ovnovollem1 39329
Description: if 𝐹 is a cover of 𝐵 in , then 𝐼 is the corresponding cover in the space of 1-dimensional reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
Hypotheses
Ref Expression
ovnovollem1.a (𝜑𝐴𝑉)
ovnovollem1.f (𝜑𝐹 ∈ ((ℝ × ℝ) ↑𝑚 ℕ))
ovnovollem1.i 𝐼 = (𝑗 ∈ ℕ ↦ {⟨𝐴, (𝐹𝑗)⟩})
ovnovollem1.s (𝜑𝐵 ran ([,) ∘ 𝐹))
ovnovollem1.b (𝜑𝐵𝑊)
ovnovollem1.z (𝜑𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
Assertion
Ref Expression
ovnovollem1 (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 {𝐴}) ↑𝑚 ℕ)((𝐵𝑚 {𝐴}) ⊆ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))))
Distinct variable groups:   𝐴,𝑖,𝑗,𝑘   𝐵,𝑖   𝑗,𝐹,𝑘   𝑖,𝐼,𝑗,𝑘   𝑘,𝑉   𝑖,𝑍   𝜑,𝑗,𝑘
Allowed substitution hints:   𝜑(𝑖)   𝐵(𝑗,𝑘)   𝐹(𝑖)   𝑉(𝑖,𝑗)   𝑊(𝑖,𝑗,𝑘)   𝑍(𝑗,𝑘)

Proof of Theorem ovnovollem1
StepHypRef Expression
1 eqidd 2610 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → {⟨𝐴, (𝐹𝑗)⟩} = {⟨𝐴, (𝐹𝑗)⟩})
2 ovnovollem1.a . . . . . . . . 9 (𝜑𝐴𝑉)
32adantr 479 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝐴𝑉)
4 ovnovollem1.f . . . . . . . . . 10 (𝜑𝐹 ∈ ((ℝ × ℝ) ↑𝑚 ℕ))
5 elmapi 7742 . . . . . . . . . 10 (𝐹 ∈ ((ℝ × ℝ) ↑𝑚 ℕ) → 𝐹:ℕ⟶(ℝ × ℝ))
64, 5syl 17 . . . . . . . . 9 (𝜑𝐹:ℕ⟶(ℝ × ℝ))
76ffvelrnda 6251 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (𝐹𝑗) ∈ (ℝ × ℝ))
8 fsng 6294 . . . . . . . 8 ((𝐴𝑉 ∧ (𝐹𝑗) ∈ (ℝ × ℝ)) → ({⟨𝐴, (𝐹𝑗)⟩}:{𝐴}⟶{(𝐹𝑗)} ↔ {⟨𝐴, (𝐹𝑗)⟩} = {⟨𝐴, (𝐹𝑗)⟩}))
93, 7, 8syl2anc 690 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹𝑗)⟩}:{𝐴}⟶{(𝐹𝑗)} ↔ {⟨𝐴, (𝐹𝑗)⟩} = {⟨𝐴, (𝐹𝑗)⟩}))
101, 9mpbird 245 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → {⟨𝐴, (𝐹𝑗)⟩}:{𝐴}⟶{(𝐹𝑗)})
117snssd 4280 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → {(𝐹𝑗)} ⊆ (ℝ × ℝ))
1210, 11fssd 5955 . . . . 5 ((𝜑𝑗 ∈ ℕ) → {⟨𝐴, (𝐹𝑗)⟩}:{𝐴}⟶(ℝ × ℝ))
13 reex 9883 . . . . . . . 8 ℝ ∈ V
1413, 13xpex 6837 . . . . . . 7 (ℝ × ℝ) ∈ V
1514a1i 11 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → (ℝ × ℝ) ∈ V)
16 snex 4829 . . . . . . 7 {𝐴} ∈ V
1716a1i 11 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → {𝐴} ∈ V)
1815, 17elmapd 7735 . . . . 5 ((𝜑𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹𝑗)⟩} ∈ ((ℝ × ℝ) ↑𝑚 {𝐴}) ↔ {⟨𝐴, (𝐹𝑗)⟩}:{𝐴}⟶(ℝ × ℝ)))
1912, 18mpbird 245 . . . 4 ((𝜑𝑗 ∈ ℕ) → {⟨𝐴, (𝐹𝑗)⟩} ∈ ((ℝ × ℝ) ↑𝑚 {𝐴}))
20 ovnovollem1.i . . . 4 𝐼 = (𝑗 ∈ ℕ ↦ {⟨𝐴, (𝐹𝑗)⟩})
2119, 20fmptd 6276 . . 3 (𝜑𝐼:ℕ⟶((ℝ × ℝ) ↑𝑚 {𝐴}))
22 ovex 6554 . . . . 5 ((ℝ × ℝ) ↑𝑚 {𝐴}) ∈ V
2322a1i 11 . . . 4 (𝜑 → ((ℝ × ℝ) ↑𝑚 {𝐴}) ∈ V)
24 nnex 10875 . . . . 5 ℕ ∈ V
2524a1i 11 . . . 4 (𝜑 → ℕ ∈ V)
2623, 25elmapd 7735 . . 3 (𝜑 → (𝐼 ∈ (((ℝ × ℝ) ↑𝑚 {𝐴}) ↑𝑚 ℕ) ↔ 𝐼:ℕ⟶((ℝ × ℝ) ↑𝑚 {𝐴})))
2721, 26mpbird 245 . 2 (𝜑𝐼 ∈ (((ℝ × ℝ) ↑𝑚 {𝐴}) ↑𝑚 ℕ))
28 ovnovollem1.s . . . . . 6 (𝜑𝐵 ran ([,) ∘ 𝐹))
29 icof 38189 . . . . . . . . . . 11 [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
3029a1i 11 . . . . . . . . . 10 (𝜑 → [,):(ℝ* × ℝ*)⟶𝒫 ℝ*)
31 rexpssxrxp 9940 . . . . . . . . . . 11 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
3231a1i 11 . . . . . . . . . 10 (𝜑 → (ℝ × ℝ) ⊆ (ℝ* × ℝ*))
3330, 32, 6fcoss 38180 . . . . . . . . 9 (𝜑 → ([,) ∘ 𝐹):ℕ⟶𝒫 ℝ*)
3433ffnd 5944 . . . . . . . 8 (𝜑 → ([,) ∘ 𝐹) Fn ℕ)
35 fniunfv 6386 . . . . . . . 8 (([,) ∘ 𝐹) Fn ℕ → 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ran ([,) ∘ 𝐹))
3634, 35syl 17 . . . . . . 7 (𝜑 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = ran ([,) ∘ 𝐹))
3736eqcomd 2615 . . . . . 6 (𝜑 ran ([,) ∘ 𝐹) = 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
3828, 37sseqtrd 3603 . . . . 5 (𝜑𝐵 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗))
39 ovnovollem1.b . . . . . 6 (𝜑𝐵𝑊)
40 fvex 6097 . . . . . . . 8 (([,) ∘ 𝐹)‘𝑗) ∈ V
4124, 40iunex 7016 . . . . . . 7 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V
4241a1i 11 . . . . . 6 (𝜑 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ∈ V)
4316a1i 11 . . . . . 6 (𝜑 → {𝐴} ∈ V)
442snn0d 38067 . . . . . 6 (𝜑 → {𝐴} ≠ ∅)
4539, 42, 43, 44mapss2 38175 . . . . 5 (𝜑 → (𝐵 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↔ (𝐵𝑚 {𝐴}) ⊆ ( 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑𝑚 {𝐴})))
4638, 45mpbid 220 . . . 4 (𝜑 → (𝐵𝑚 {𝐴}) ⊆ ( 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑𝑚 {𝐴}))
47 nfv 1829 . . . . . . 7 𝑗𝜑
48 fvex 6097 . . . . . . . 8 ([,)‘(𝐹𝑗)) ∈ V
4948a1i 11 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ([,)‘(𝐹𝑗)) ∈ V)
5047, 25, 49, 2iunmapsn 38187 . . . . . 6 (𝜑 𝑗 ∈ ℕ (([,)‘(𝐹𝑗)) ↑𝑚 {𝐴}) = ( 𝑗 ∈ ℕ ([,)‘(𝐹𝑗)) ↑𝑚 {𝐴}))
5150eqcomd 2615 . . . . 5 (𝜑 → ( 𝑗 ∈ ℕ ([,)‘(𝐹𝑗)) ↑𝑚 {𝐴}) = 𝑗 ∈ ℕ (([,)‘(𝐹𝑗)) ↑𝑚 {𝐴}))
52 elmapfun 7744 . . . . . . . . . 10 (𝐹 ∈ ((ℝ × ℝ) ↑𝑚 ℕ) → Fun 𝐹)
534, 52syl 17 . . . . . . . . 9 (𝜑 → Fun 𝐹)
5453adantr 479 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → Fun 𝐹)
55 simpr 475 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
56 fdm 5949 . . . . . . . . . . . 12 (𝐹:ℕ⟶(ℝ × ℝ) → dom 𝐹 = ℕ)
576, 56syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = ℕ)
5857eqcomd 2615 . . . . . . . . . 10 (𝜑 → ℕ = dom 𝐹)
5958adantr 479 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → ℕ = dom 𝐹)
6055, 59eleqtrd 2689 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ dom 𝐹)
61 fvco 6168 . . . . . . . 8 ((Fun 𝐹𝑗 ∈ dom 𝐹) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹𝑗)))
6254, 60, 61syl2anc 690 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (([,) ∘ 𝐹)‘𝑗) = ([,)‘(𝐹𝑗)))
6362iuneq2dv 4472 . . . . . 6 (𝜑 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) = 𝑗 ∈ ℕ ([,)‘(𝐹𝑗)))
6463oveq1d 6541 . . . . 5 (𝜑 → ( 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑𝑚 {𝐴}) = ( 𝑗 ∈ ℕ ([,)‘(𝐹𝑗)) ↑𝑚 {𝐴}))
65 ffun 5946 . . . . . . . . . . . . 13 ({⟨𝐴, (𝐹𝑗)⟩}:{𝐴}⟶{(𝐹𝑗)} → Fun {⟨𝐴, (𝐹𝑗)⟩})
6610, 65syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → Fun {⟨𝐴, (𝐹𝑗)⟩})
67 id 22 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ)
68 snex 4829 . . . . . . . . . . . . . . . 16 {⟨𝐴, (𝐹𝑗)⟩} ∈ V
6968a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → {⟨𝐴, (𝐹𝑗)⟩} ∈ V)
7020fvmpt2 6184 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℕ ∧ {⟨𝐴, (𝐹𝑗)⟩} ∈ V) → (𝐼𝑗) = {⟨𝐴, (𝐹𝑗)⟩})
7167, 69, 70syl2anc 690 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ → (𝐼𝑗) = {⟨𝐴, (𝐹𝑗)⟩})
7271adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (𝐼𝑗) = {⟨𝐴, (𝐹𝑗)⟩})
7372funeqd 5810 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (Fun (𝐼𝑗) ↔ Fun {⟨𝐴, (𝐹𝑗)⟩}))
7466, 73mpbird 245 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → Fun (𝐼𝑗))
7574adantr 479 . . . . . . . . . 10 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → Fun (𝐼𝑗))
76 simpr 475 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ {𝐴})
7772dmeqd 5234 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → dom (𝐼𝑗) = dom {⟨𝐴, (𝐹𝑗)⟩})
78 fdm 5949 . . . . . . . . . . . . . . 15 ({⟨𝐴, (𝐹𝑗)⟩}:{𝐴}⟶(ℝ × ℝ) → dom {⟨𝐴, (𝐹𝑗)⟩} = {𝐴})
7912, 78syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → dom {⟨𝐴, (𝐹𝑗)⟩} = {𝐴})
8077, 79eqtrd 2643 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → dom (𝐼𝑗) = {𝐴})
8180eleq2d 2672 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (𝑘 ∈ dom (𝐼𝑗) ↔ 𝑘 ∈ {𝐴}))
8281adantr 479 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (𝑘 ∈ dom (𝐼𝑗) ↔ 𝑘 ∈ {𝐴}))
8376, 82mpbird 245 . . . . . . . . . 10 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → 𝑘 ∈ dom (𝐼𝑗))
84 fvco 6168 . . . . . . . . . 10 ((Fun (𝐼𝑗) ∧ 𝑘 ∈ dom (𝐼𝑗)) → (([,) ∘ (𝐼𝑗))‘𝑘) = ([,)‘((𝐼𝑗)‘𝑘)))
8575, 83, 84syl2anc 690 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼𝑗))‘𝑘) = ([,)‘((𝐼𝑗)‘𝑘)))
8671fveq1d 6089 . . . . . . . . . . . 12 (𝑗 ∈ ℕ → ((𝐼𝑗)‘𝑘) = ({⟨𝐴, (𝐹𝑗)⟩}‘𝑘))
8786ad2antlr 758 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼𝑗)‘𝑘) = ({⟨𝐴, (𝐹𝑗)⟩}‘𝑘))
88 elsni 4141 . . . . . . . . . . . . 13 (𝑘 ∈ {𝐴} → 𝑘 = 𝐴)
8988fveq2d 6091 . . . . . . . . . . . 12 (𝑘 ∈ {𝐴} → ({⟨𝐴, (𝐹𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹𝑗)⟩}‘𝐴))
9089adantl 480 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹𝑗)⟩}‘𝑘) = ({⟨𝐴, (𝐹𝑗)⟩}‘𝐴))
91 fvex 6097 . . . . . . . . . . . . . 14 (𝐹𝑗) ∈ V
9291a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑗) ∈ V)
93 fvsng 6329 . . . . . . . . . . . . 13 ((𝐴𝑉 ∧ (𝐹𝑗) ∈ V) → ({⟨𝐴, (𝐹𝑗)⟩}‘𝐴) = (𝐹𝑗))
942, 92, 93syl2anc 690 . . . . . . . . . . . 12 (𝜑 → ({⟨𝐴, (𝐹𝑗)⟩}‘𝐴) = (𝐹𝑗))
9594ad2antrr 757 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ({⟨𝐴, (𝐹𝑗)⟩}‘𝐴) = (𝐹𝑗))
9687, 90, 953eqtrd 2647 . . . . . . . . . 10 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ((𝐼𝑗)‘𝑘) = (𝐹𝑗))
9796fveq2d 6091 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘((𝐼𝑗)‘𝑘)) = ([,)‘(𝐹𝑗)))
98 eqidd 2610 . . . . . . . . 9 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → ([,)‘(𝐹𝑗)) = ([,)‘(𝐹𝑗)))
9985, 97, 983eqtrd 2647 . . . . . . . 8 (((𝜑𝑗 ∈ ℕ) ∧ 𝑘 ∈ {𝐴}) → (([,) ∘ (𝐼𝑗))‘𝑘) = ([,)‘(𝐹𝑗)))
10099ixpeq2dva 7786 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘) = X𝑘 ∈ {𝐴} ([,)‘(𝐹𝑗)))
10116, 48ixpconst 7781 . . . . . . . 8 X𝑘 ∈ {𝐴} ([,)‘(𝐹𝑗)) = (([,)‘(𝐹𝑗)) ↑𝑚 {𝐴})
102101a1i 11 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} ([,)‘(𝐹𝑗)) = (([,)‘(𝐹𝑗)) ↑𝑚 {𝐴}))
103100, 102eqtrd 2643 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘) = (([,)‘(𝐹𝑗)) ↑𝑚 {𝐴}))
104103iuneq2dv 4472 . . . . 5 (𝜑 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘) = 𝑗 ∈ ℕ (([,)‘(𝐹𝑗)) ↑𝑚 {𝐴}))
10551, 64, 1043eqtr4d 2653 . . . 4 (𝜑 → ( 𝑗 ∈ ℕ (([,) ∘ 𝐹)‘𝑗) ↑𝑚 {𝐴}) = 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘))
10646, 105sseqtrd 3603 . . 3 (𝜑 → (𝐵𝑚 {𝐴}) ⊆ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘))
107 ovnovollem1.z . . . 4 (𝜑𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹)))
108 nfcv 2750 . . . . . . 7 𝑗𝐹
109 ressxr 9939 . . . . . . . . . 10 ℝ ⊆ ℝ*
110 xpss2 5140 . . . . . . . . . 10 (ℝ ⊆ ℝ* → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
111109, 110ax-mp 5 . . . . . . . . 9 (ℝ × ℝ) ⊆ (ℝ × ℝ*)
112111a1i 11 . . . . . . . 8 (𝜑 → (ℝ × ℝ) ⊆ (ℝ × ℝ*))
1136, 112fssd 5955 . . . . . . 7 (𝜑𝐹:ℕ⟶(ℝ × ℝ*))
114108, 113volicofmpt 38673 . . . . . 6 (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗))))))
11571coeq2d 5193 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → ([,) ∘ (𝐼𝑗)) = ([,) ∘ {⟨𝐴, (𝐹𝑗)⟩}))
116115fveq1d 6089 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ → (([,) ∘ (𝐼𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹𝑗)⟩})‘𝐴))
117116adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (([,) ∘ (𝐼𝑗))‘𝐴) = (([,) ∘ {⟨𝐴, (𝐹𝑗)⟩})‘𝐴))
118 snidg 4152 . . . . . . . . . . . . . . . . 17 (𝐴𝑉𝐴 ∈ {𝐴})
1192, 118syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ {𝐴})
120 dmsnopg 5509 . . . . . . . . . . . . . . . . 17 ((𝐹𝑗) ∈ V → dom {⟨𝐴, (𝐹𝑗)⟩} = {𝐴})
12192, 120syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → dom {⟨𝐴, (𝐹𝑗)⟩} = {𝐴})
122119, 121eleqtrrd 2690 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ dom {⟨𝐴, (𝐹𝑗)⟩})
123122adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → 𝐴 ∈ dom {⟨𝐴, (𝐹𝑗)⟩})
124 fvco 6168 . . . . . . . . . . . . . 14 ((Fun {⟨𝐴, (𝐹𝑗)⟩} ∧ 𝐴 ∈ dom {⟨𝐴, (𝐹𝑗)⟩}) → (([,) ∘ {⟨𝐴, (𝐹𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹𝑗)⟩}‘𝐴)))
12566, 123, 124syl2anc 690 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (([,) ∘ {⟨𝐴, (𝐹𝑗)⟩})‘𝐴) = ([,)‘({⟨𝐴, (𝐹𝑗)⟩}‘𝐴)))
12691a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ) → (𝐹𝑗) ∈ V)
1273, 126, 93syl2anc 690 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹𝑗)⟩}‘𝐴) = (𝐹𝑗))
128 1st2nd2 7073 . . . . . . . . . . . . . . . . 17 ((𝐹𝑗) ∈ (ℝ × ℝ) → (𝐹𝑗) = ⟨(1st ‘(𝐹𝑗)), (2nd ‘(𝐹𝑗))⟩)
1297, 128syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ) → (𝐹𝑗) = ⟨(1st ‘(𝐹𝑗)), (2nd ‘(𝐹𝑗))⟩)
130127, 129eqtrd 2643 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ) → ({⟨𝐴, (𝐹𝑗)⟩}‘𝐴) = ⟨(1st ‘(𝐹𝑗)), (2nd ‘(𝐹𝑗))⟩)
131130fveq2d 6091 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹𝑗)⟩}‘𝐴)) = ([,)‘⟨(1st ‘(𝐹𝑗)), (2nd ‘(𝐹𝑗))⟩))
132 df-ov 6529 . . . . . . . . . . . . . . . 16 ((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗))) = ([,)‘⟨(1st ‘(𝐹𝑗)), (2nd ‘(𝐹𝑗))⟩)
133132eqcomi 2618 . . . . . . . . . . . . . . 15 ([,)‘⟨(1st ‘(𝐹𝑗)), (2nd ‘(𝐹𝑗))⟩) = ((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗)))
134133a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ([,)‘⟨(1st ‘(𝐹𝑗)), (2nd ‘(𝐹𝑗))⟩) = ((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗))))
135131, 134eqtrd 2643 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → ([,)‘({⟨𝐴, (𝐹𝑗)⟩}‘𝐴)) = ((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗))))
136117, 125, 1353eqtrd 2647 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (([,) ∘ (𝐼𝑗))‘𝐴) = ((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗))))
137136fveq2d 6091 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼𝑗))‘𝐴)) = (vol‘((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗)))))
138 xp1st 7066 . . . . . . . . . . . . 13 ((𝐹𝑗) ∈ (ℝ × ℝ) → (1st ‘(𝐹𝑗)) ∈ ℝ)
1397, 138syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (1st ‘(𝐹𝑗)) ∈ ℝ)
140 xp2nd 7067 . . . . . . . . . . . . 13 ((𝐹𝑗) ∈ (ℝ × ℝ) → (2nd ‘(𝐹𝑗)) ∈ ℝ)
1417, 140syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → (2nd ‘(𝐹𝑗)) ∈ ℝ)
142 volicore 39254 . . . . . . . . . . . 12 (((1st ‘(𝐹𝑗)) ∈ ℝ ∧ (2nd ‘(𝐹𝑗)) ∈ ℝ) → (vol‘((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗)))) ∈ ℝ)
143139, 141, 142syl2anc 690 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗)))) ∈ ℝ)
144137, 143eqeltrd 2687 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼𝑗))‘𝐴)) ∈ ℝ)
145144recnd 9924 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (vol‘(([,) ∘ (𝐼𝑗))‘𝐴)) ∈ ℂ)
146 fveq2 6087 . . . . . . . . . . 11 (𝑘 = 𝐴 → (([,) ∘ (𝐼𝑗))‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝐴))
147146fveq2d 6091 . . . . . . . . . 10 (𝑘 = 𝐴 → (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼𝑗))‘𝐴)))
148147prodsn 14479 . . . . . . . . 9 ((𝐴𝑉 ∧ (vol‘(([,) ∘ (𝐼𝑗))‘𝐴)) ∈ ℂ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼𝑗))‘𝐴)))
1493, 145, 148syl2anc 690 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼𝑗))‘𝐴)))
150149, 137eqtr2d 2644 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → (vol‘((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗)))) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)))
151150mpteq2dva 4666 . . . . . 6 (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((1st ‘(𝐹𝑗))[,)(2nd ‘(𝐹𝑗))))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘))))
152114, 151eqtrd 2643 . . . . 5 (𝜑 → ((vol ∘ [,)) ∘ 𝐹) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘))))
153152fveq2d 6091 . . . 4 (𝜑 → (Σ^‘((vol ∘ [,)) ∘ 𝐹)) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)))))
154107, 153eqtrd 2643 . . 3 (𝜑𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)))))
155106, 154jca 552 . 2 (𝜑 → ((𝐵𝑚 {𝐴}) ⊆ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘))))))
156 fveq1 6086 . . . . . . . . 9 (𝑖 = 𝐼 → (𝑖𝑗) = (𝐼𝑗))
157156coeq2d 5193 . . . . . . . 8 (𝑖 = 𝐼 → ([,) ∘ (𝑖𝑗)) = ([,) ∘ (𝐼𝑗)))
158157fveq1d 6089 . . . . . . 7 (𝑖 = 𝐼 → (([,) ∘ (𝑖𝑗))‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝑘))
159158ixpeq2dv 7787 . . . . . 6 (𝑖 = 𝐼X𝑘 ∈ {𝐴} (([,) ∘ (𝑖𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘))
160159iuneq2d 4477 . . . . 5 (𝑖 = 𝐼 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖𝑗))‘𝑘) = 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘))
161160sseq2d 3595 . . . 4 (𝑖 = 𝐼 → ((𝐵𝑚 {𝐴}) ⊆ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖𝑗))‘𝑘) ↔ (𝐵𝑚 {𝐴}) ⊆ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘)))
162 simpl 471 . . . . . . . . . . . 12 ((𝑖 = 𝐼𝑘 ∈ {𝐴}) → 𝑖 = 𝐼)
163162fveq1d 6089 . . . . . . . . . . 11 ((𝑖 = 𝐼𝑘 ∈ {𝐴}) → (𝑖𝑗) = (𝐼𝑗))
164163coeq2d 5193 . . . . . . . . . 10 ((𝑖 = 𝐼𝑘 ∈ {𝐴}) → ([,) ∘ (𝑖𝑗)) = ([,) ∘ (𝐼𝑗)))
165164fveq1d 6089 . . . . . . . . 9 ((𝑖 = 𝐼𝑘 ∈ {𝐴}) → (([,) ∘ (𝑖𝑗))‘𝑘) = (([,) ∘ (𝐼𝑗))‘𝑘))
166165fveq2d 6091 . . . . . . . 8 ((𝑖 = 𝐼𝑘 ∈ {𝐴}) → (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)))
167166prodeq2dv 14440 . . . . . . 7 (𝑖 = 𝐼 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)))
168167mpteq2dv 4667 . . . . . 6 (𝑖 = 𝐼 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘))))
169168fveq2d 6091 . . . . 5 (𝑖 = 𝐼 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))) = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)))))
170169eqeq2d 2619 . . . 4 (𝑖 = 𝐼 → (𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))) ↔ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘))))))
171161, 170anbi12d 742 . . 3 (𝑖 = 𝐼 → (((𝐵𝑚 {𝐴}) ⊆ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))) ↔ ((𝐵𝑚 {𝐴}) ⊆ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)))))))
172171rspcev 3281 . 2 ((𝐼 ∈ (((ℝ × ℝ) ↑𝑚 {𝐴}) ↑𝑚 ℕ) ∧ ((𝐵𝑚 {𝐴}) ⊆ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 {𝐴}) ↑𝑚 ℕ)((𝐵𝑚 {𝐴}) ⊆ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))))
17327, 155, 172syl2anc 690 1 (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 {𝐴}) ↑𝑚 ℕ)((𝐵𝑚 {𝐴}) ⊆ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖𝑗))‘𝑘))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wrex 2896  Vcvv 3172  wss 3539  𝒫 cpw 4107  {csn 4124  cop 4130   cuni 4366   ciun 4449  cmpt 4637   × cxp 5025  dom cdm 5027  ran crn 5028  ccom 5031  Fun wfun 5783   Fn wfn 5784  wf 5785  cfv 5789  (class class class)co 6526  1st c1st 7034  2nd c2nd 7035  𝑚 cmap 7721  Xcixp 7771  cc 9790  cr 9791  *cxr 9929  cn 10869  [,)cico 12006  cprod 14422  volcvol 22983  Σ^csumge0 39038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-se 4987  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-isom 5798  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10536  df-nn 10870  df-2 10928  df-3 10929  df-n0 11142  df-z 11213  df-uz 11522  df-q 11623  df-rp 11667  df-xneg 11780  df-xadd 11781  df-xmul 11782  df-ioo 12008  df-ico 12010  df-icc 12011  df-fz 12155  df-fzo 12292  df-fl 12412  df-seq 12621  df-exp 12680  df-hash 12937  df-cj 13635  df-re 13636  df-im 13637  df-sqrt 13771  df-abs 13772  df-clim 14015  df-rlim 14016  df-sum 14213  df-prod 14423  df-rest 15854  df-topgen 15875  df-psmet 19507  df-xmet 19508  df-met 19509  df-bl 19510  df-mopn 19511  df-top 20468  df-bases 20469  df-topon 20470  df-cmp 20947  df-ovol 22984  df-vol 22985
This theorem is referenced by:  ovnovollem3  39331
  Copyright terms: Public domain W3C validator