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

Theorem ovolval4lem1 46096
Description: |- ( ( ph /\ n e. A ) -> ( ( (,) o. G ) 𝑛) = (((,) ∘ 𝐹) n ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.)
Hypotheses
Ref Expression
ovolval4lem1.f (πœ‘ β†’ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*))
ovolval4lem1.g 𝐺 = (𝑛 ∈ β„• ↦ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩)
ovolval4lem1.a 𝐴 = {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))}
Assertion
Ref Expression
ovolval4lem1 (πœ‘ β†’ (βˆͺ ran ((,) ∘ 𝐹) = βˆͺ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺))))
Distinct variable groups:   𝐴,𝑛   𝑛,𝐹   𝑛,𝐺   πœ‘,𝑛

Proof of Theorem ovolval4lem1
StepHypRef Expression
1 ioof 13451 . . . . . . . 8 (,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ
21a1i 11 . . . . . . 7 (πœ‘ β†’ (,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ)
3 ovolval4lem1.f . . . . . . 7 (πœ‘ β†’ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*))
4 fco 6741 . . . . . . 7 (((,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ ∧ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*)) β†’ ((,) ∘ 𝐹):β„•βŸΆπ’« ℝ)
52, 3, 4syl2anc 582 . . . . . 6 (πœ‘ β†’ ((,) ∘ 𝐹):β„•βŸΆπ’« ℝ)
65ffnd 6718 . . . . 5 (πœ‘ β†’ ((,) ∘ 𝐹) Fn β„•)
7 fniunfv 7251 . . . . 5 (((,) ∘ 𝐹) Fn β„• β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) = βˆͺ ran ((,) ∘ 𝐹))
86, 7syl 17 . . . 4 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) = βˆͺ ran ((,) ∘ 𝐹))
98eqcomd 2731 . . 3 (πœ‘ β†’ βˆͺ ran ((,) ∘ 𝐹) = βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›))
10 ovolval4lem1.a . . . . . . . . 9 𝐴 = {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))}
11 ssrab2 4070 . . . . . . . . 9 {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))} βŠ† β„•
1210, 11eqsstri 4008 . . . . . . . 8 𝐴 βŠ† β„•
13 undif 4478 . . . . . . . 8 (𝐴 βŠ† β„• ↔ (𝐴 βˆͺ (β„• βˆ– 𝐴)) = β„•)
1412, 13mpbi 229 . . . . . . 7 (𝐴 βˆͺ (β„• βˆ– 𝐴)) = β„•
1514eqcomi 2734 . . . . . 6 β„• = (𝐴 βˆͺ (β„• βˆ– 𝐴))
1615iuneq1i 44512 . . . . 5 βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) = βˆͺ 𝑛 ∈ (𝐴 βˆͺ (β„• βˆ– 𝐴))(((,) ∘ 𝐹)β€˜π‘›)
17 iunxun 5093 . . . . 5 βˆͺ 𝑛 ∈ (𝐴 βˆͺ (β„• βˆ– 𝐴))(((,) ∘ 𝐹)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›))
1816, 17eqtri 2753 . . . 4 βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›))
1918a1i 11 . . 3 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›)))
203ffvelcdmda 7087 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ (ℝ* Γ— ℝ*))
21 xp1st 8019 . . . . . . . . . . 11 ((πΉβ€˜π‘›) ∈ (ℝ* Γ— ℝ*) β†’ (1st β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
2220, 21syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (1st β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
23 xp2nd 8020 . . . . . . . . . . . 12 ((πΉβ€˜π‘›) ∈ (ℝ* Γ— ℝ*) β†’ (2nd β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
2420, 23syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (2nd β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
2524, 22ifcld 4571 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))) ∈ ℝ*)
2622, 25opelxpd 5712 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩ ∈ (ℝ* Γ— ℝ*))
27 ovolval4lem1.g . . . . . . . . 9 𝐺 = (𝑛 ∈ β„• ↦ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩)
2826, 27fmptd 7117 . . . . . . . 8 (πœ‘ β†’ 𝐺:β„•βŸΆ(ℝ* Γ— ℝ*))
29 fco 6741 . . . . . . . 8 (((,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ ∧ 𝐺:β„•βŸΆ(ℝ* Γ— ℝ*)) β†’ ((,) ∘ 𝐺):β„•βŸΆπ’« ℝ)
302, 28, 29syl2anc 582 . . . . . . 7 (πœ‘ β†’ ((,) ∘ 𝐺):β„•βŸΆπ’« ℝ)
3130ffnd 6718 . . . . . 6 (πœ‘ β†’ ((,) ∘ 𝐺) Fn β„•)
32 fniunfv 7251 . . . . . 6 (((,) ∘ 𝐺) Fn β„• β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) = βˆͺ ran ((,) ∘ 𝐺))
3331, 32syl 17 . . . . 5 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) = βˆͺ ran ((,) ∘ 𝐺))
3433eqcomd 2731 . . . 4 (πœ‘ β†’ βˆͺ ran ((,) ∘ 𝐺) = βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›))
3515iuneq1i 44512 . . . . . 6 βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) = βˆͺ 𝑛 ∈ (𝐴 βˆͺ (β„• βˆ– 𝐴))(((,) ∘ 𝐺)β€˜π‘›)
36 iunxun 5093 . . . . . 6 βˆͺ 𝑛 ∈ (𝐴 βˆͺ (β„• βˆ– 𝐴))(((,) ∘ 𝐺)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›))
3735, 36eqtri 2753 . . . . 5 βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›))
3837a1i 11 . . . 4 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›)))
3928adantr 479 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ 𝐺:β„•βŸΆ(ℝ* Γ— ℝ*))
4012sseli 3969 . . . . . . . . 9 (𝑛 ∈ 𝐴 β†’ 𝑛 ∈ β„•)
4140adantl 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ 𝑛 ∈ β„•)
42 fvco3 6990 . . . . . . . 8 ((𝐺:β„•βŸΆ(ℝ* Γ— ℝ*) ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐺)β€˜π‘›) = ((,)β€˜(πΊβ€˜π‘›)))
4339, 41, 42syl2anc 582 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐺)β€˜π‘›) = ((,)β€˜(πΊβ€˜π‘›)))
443adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*))
45 fvco3 6990 . . . . . . . . 9 ((𝐹:β„•βŸΆ(ℝ* Γ— ℝ*) ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((,)β€˜(πΉβ€˜π‘›)))
4644, 41, 45syl2anc 582 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((,)β€˜(πΉβ€˜π‘›)))
47 simpl 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ πœ‘)
48 1st2nd2 8026 . . . . . . . . . . . 12 ((πΉβ€˜π‘›) ∈ (ℝ* Γ— ℝ*) β†’ (πΉβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
4920, 48syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
5047, 41, 49syl2anc 582 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (πΉβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
5127a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐺 = (𝑛 ∈ β„• ↦ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩))
5226elexd 3485 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩ ∈ V)
5351, 52fvmpt2d 7011 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΊβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩)
5447, 41, 53syl2anc 582 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (πΊβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩)
5510eleq2i 2817 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))})
5655biimpi 215 . . . . . . . . . . . . . . . 16 (𝑛 ∈ 𝐴 β†’ 𝑛 ∈ {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))})
57 rabid 3440 . . . . . . . . . . . . . . . 16 (𝑛 ∈ {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))} ↔ (𝑛 ∈ β„• ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))))
5856, 57sylib 217 . . . . . . . . . . . . . . 15 (𝑛 ∈ 𝐴 β†’ (𝑛 ∈ β„• ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))))
5958simprd 494 . . . . . . . . . . . . . 14 (𝑛 ∈ 𝐴 β†’ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)))
6059adantl 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)))
6160iftrued 4533 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))) = (2nd β€˜(πΉβ€˜π‘›)))
6261opeq2d 4877 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩ = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
63 eqidd 2726 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩ = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
6454, 62, 633eqtrd 2769 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (πΊβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
6550, 64eqtr4d 2768 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (πΉβ€˜π‘›) = (πΊβ€˜π‘›))
6665fveq2d 6894 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ ((,)β€˜(πΉβ€˜π‘›)) = ((,)β€˜(πΊβ€˜π‘›)))
6746, 66eqtrd 2765 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((,)β€˜(πΊβ€˜π‘›)))
6843, 67eqtr4d 2768 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐺)β€˜π‘›) = (((,) ∘ 𝐹)β€˜π‘›))
6968iuneq2dv 5016 . . . . 5 (πœ‘ β†’ βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)β€˜π‘›) = βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›))
7028adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ 𝐺:β„•βŸΆ(ℝ* Γ— ℝ*))
71 eldifi 4120 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– 𝐴) β†’ 𝑛 ∈ β„•)
7271adantl 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ 𝑛 ∈ β„•)
7370, 72, 42syl2anc 582 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐺)β€˜π‘›) = ((,)β€˜(πΊβ€˜π‘›)))
74 simpl 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ πœ‘)
7574, 72, 53syl2anc 582 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (πΊβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩)
7671anim1i 613 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (β„• βˆ– 𝐴) ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))) β†’ (𝑛 ∈ β„• ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))))
7776, 57sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (β„• βˆ– 𝐴) ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))) β†’ 𝑛 ∈ {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))})
7877, 55sylibr 233 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (β„• βˆ– 𝐴) ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))) β†’ 𝑛 ∈ 𝐴)
7978adantll 712 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))) β†’ 𝑛 ∈ 𝐴)
80 eldifn 4121 . . . . . . . . . . . . . . 15 (𝑛 ∈ (β„• βˆ– 𝐴) β†’ Β¬ 𝑛 ∈ 𝐴)
8180ad2antlr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))) β†’ Β¬ 𝑛 ∈ 𝐴)
8279, 81pm2.65da 815 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ Β¬ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)))
8382iffalsed 4536 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))) = (1st β€˜(πΉβ€˜π‘›)))
8483opeq2d 4877 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩ = ⟨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩)
8575, 84eqtrd 2765 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (πΊβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩)
8685fveq2d 6894 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((,)β€˜(πΊβ€˜π‘›)) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩))
87 iooid 13379 . . . . . . . . . . . 12 ((1st β€˜(πΉβ€˜π‘›))(,)(1st β€˜(πΉβ€˜π‘›))) = βˆ…
8887eqcomi 2734 . . . . . . . . . . 11 βˆ… = ((1st β€˜(πΉβ€˜π‘›))(,)(1st β€˜(πΉβ€˜π‘›)))
89 df-ov 7416 . . . . . . . . . . 11 ((1st β€˜(πΉβ€˜π‘›))(,)(1st β€˜(πΉβ€˜π‘›))) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩)
9088, 89eqtr2i 2754 . . . . . . . . . 10 ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩) = βˆ…
9190a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩) = βˆ…)
9273, 86, 913eqtrd 2769 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐺)β€˜π‘›) = βˆ…)
9392iuneq2dv 5016 . . . . . . 7 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›) = βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)βˆ…)
94 iun0 5061 . . . . . . . 8 βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)βˆ… = βˆ…
9594a1i 11 . . . . . . 7 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)βˆ… = βˆ…)
9693, 95eqtrd 2765 . . . . . 6 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›) = βˆ…)
9774, 3syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*))
9897, 72, 45syl2anc 582 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((,)β€˜(πΉβ€˜π‘›)))
9974, 72, 49syl2anc 582 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (πΉβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
10099fveq2d 6894 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((,)β€˜(πΉβ€˜π‘›)) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩))
101 df-ov 7416 . . . . . . . . . . 11 ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
102101a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩))
103 simplr 767 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ 𝑛 ∈ (β„• βˆ– 𝐴))
10472, 22syldan 589 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (1st β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
105104adantr 479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ (1st β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
10672, 24syldan 589 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (2nd β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
107106adantr 479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ (2nd β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
108 simpr 483 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›)))
109105, 107xrltnled 44804 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ ((1st β€˜(πΉβ€˜π‘›)) < (2nd β€˜(πΉβ€˜π‘›)) ↔ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))))
110108, 109mpbird 256 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ (1st β€˜(πΉβ€˜π‘›)) < (2nd β€˜(πΉβ€˜π‘›)))
111105, 107, 110xrltled 13156 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)))
112103, 111, 78syl2anc 582 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ 𝑛 ∈ 𝐴)
11380ad2antlr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ Β¬ 𝑛 ∈ 𝐴)
114112, 113condan 816 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›)))
115 ioo0 13376 . . . . . . . . . . . 12 (((1st β€˜(πΉβ€˜π‘›)) ∈ ℝ* ∧ (2nd β€˜(πΉβ€˜π‘›)) ∈ ℝ*) β†’ (((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) = βˆ… ↔ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))))
116104, 106, 115syl2anc 582 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) = βˆ… ↔ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))))
117114, 116mpbird 256 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) = βˆ…)
118102, 117eqtr3d 2767 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩) = βˆ…)
11998, 100, 1183eqtrd 2769 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐹)β€˜π‘›) = βˆ…)
120119iuneq2dv 5016 . . . . . . 7 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›) = βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)βˆ…)
121120, 95eqtrd 2765 . . . . . 6 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›) = βˆ…)
12296, 121eqtr4d 2768 . . . . 5 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›) = βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›))
12369, 122uneq12d 4158 . . . 4 (πœ‘ β†’ (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›)) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›)))
12434, 38, 1233eqtrrd 2770 . . 3 (πœ‘ β†’ (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›)) = βˆͺ ran ((,) ∘ 𝐺))
1259, 19, 1243eqtrd 2769 . 2 (πœ‘ β†’ βˆͺ ran ((,) ∘ 𝐹) = βˆͺ ran ((,) ∘ 𝐺))
126 volf 25471 . . . . . 6 vol:dom vol⟢(0[,]+∞)
127126a1i 11 . . . . 5 (πœ‘ β†’ vol:dom vol⟢(0[,]+∞))
1283adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*))
129 simpr 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
130128, 129, 45syl2anc 582 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((,)β€˜(πΉβ€˜π‘›)))
13149fveq2d 6894 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((,)β€˜(πΉβ€˜π‘›)) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩))
132101eqcomi 2734 . . . . . . . . . . 11 ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩) = ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›)))
133132a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩) = ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))))
134130, 131, 1333eqtrd 2769 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))))
135 ioombl 25507 . . . . . . . . . 10 ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) ∈ dom vol
136135a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) ∈ dom vol)
137134, 136eqeltrd 2825 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐹)β€˜π‘›) ∈ dom vol)
138137ralrimiva 3136 . . . . . . 7 (πœ‘ β†’ βˆ€π‘› ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) ∈ dom vol)
1396, 138jca 510 . . . . . 6 (πœ‘ β†’ (((,) ∘ 𝐹) Fn β„• ∧ βˆ€π‘› ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) ∈ dom vol))
140 ffnfv 7122 . . . . . 6 (((,) ∘ 𝐹):β„•βŸΆdom vol ↔ (((,) ∘ 𝐹) Fn β„• ∧ βˆ€π‘› ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) ∈ dom vol))
141139, 140sylibr 233 . . . . 5 (πœ‘ β†’ ((,) ∘ 𝐹):β„•βŸΆdom vol)
142 fco 6741 . . . . 5 ((vol:dom vol⟢(0[,]+∞) ∧ ((,) ∘ 𝐹):β„•βŸΆdom vol) β†’ (vol ∘ ((,) ∘ 𝐹)):β„•βŸΆ(0[,]+∞))
143127, 141, 142syl2anc 582 . . . 4 (πœ‘ β†’ (vol ∘ ((,) ∘ 𝐹)):β„•βŸΆ(0[,]+∞))
144143ffnd 6718 . . 3 (πœ‘ β†’ (vol ∘ ((,) ∘ 𝐹)) Fn β„•)
14568adantlr 713 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐺)β€˜π‘›) = (((,) ∘ 𝐹)β€˜π‘›))
146137adantr 479 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐹)β€˜π‘›) ∈ dom vol)
147145, 146eqeltrd 2825 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol)
148 simpll 765 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ Β¬ 𝑛 ∈ 𝐴) β†’ πœ‘)
149 eldif 3951 . . . . . . . . . . . . 13 (𝑛 ∈ (β„• βˆ– 𝐴) ↔ (𝑛 ∈ β„• ∧ Β¬ 𝑛 ∈ 𝐴))
150149bicomi 223 . . . . . . . . . . . 12 ((𝑛 ∈ β„• ∧ Β¬ 𝑛 ∈ 𝐴) ↔ 𝑛 ∈ (β„• βˆ– 𝐴))
151150biimpi 215 . . . . . . . . . . 11 ((𝑛 ∈ β„• ∧ Β¬ 𝑛 ∈ 𝐴) β†’ 𝑛 ∈ (β„• βˆ– 𝐴))
152151adantll 712 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ Β¬ 𝑛 ∈ 𝐴) β†’ 𝑛 ∈ (β„• βˆ– 𝐴))
153117, 135eqeltrrdi 2834 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ βˆ… ∈ dom vol)
15492, 153eqeltrd 2825 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol)
155148, 152, 154syl2anc 582 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ Β¬ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol)
156147, 155pm2.61dan 811 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol)
157156ralrimiva 3136 . . . . . . 7 (πœ‘ β†’ βˆ€π‘› ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol)
15831, 157jca 510 . . . . . 6 (πœ‘ β†’ (((,) ∘ 𝐺) Fn β„• ∧ βˆ€π‘› ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol))
159 ffnfv 7122 . . . . . 6 (((,) ∘ 𝐺):β„•βŸΆdom vol ↔ (((,) ∘ 𝐺) Fn β„• ∧ βˆ€π‘› ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol))
160158, 159sylibr 233 . . . . 5 (πœ‘ β†’ ((,) ∘ 𝐺):β„•βŸΆdom vol)
161 fco 6741 . . . . 5 ((vol:dom vol⟢(0[,]+∞) ∧ ((,) ∘ 𝐺):β„•βŸΆdom vol) β†’ (vol ∘ ((,) ∘ 𝐺)):β„•βŸΆ(0[,]+∞))
162127, 160, 161syl2anc 582 . . . 4 (πœ‘ β†’ (vol ∘ ((,) ∘ 𝐺)):β„•βŸΆ(0[,]+∞))
163162ffnd 6718 . . 3 (πœ‘ β†’ (vol ∘ ((,) ∘ 𝐺)) Fn β„•)
164145eqcomd 2731 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐹)β€˜π‘›) = (((,) ∘ 𝐺)β€˜π‘›))
165119, 92eqtr4d 2768 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐹)β€˜π‘›) = (((,) ∘ 𝐺)β€˜π‘›))
166148, 152, 165syl2anc 582 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ Β¬ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐹)β€˜π‘›) = (((,) ∘ 𝐺)β€˜π‘›))
167164, 166pm2.61dan 811 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐹)β€˜π‘›) = (((,) ∘ 𝐺)β€˜π‘›))
168167fveq2d 6894 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (volβ€˜(((,) ∘ 𝐹)β€˜π‘›)) = (volβ€˜(((,) ∘ 𝐺)β€˜π‘›)))
169 fnfun 6649 . . . . . . 7 (((,) ∘ 𝐹) Fn β„• β†’ Fun ((,) ∘ 𝐹))
1706, 169syl 17 . . . . . 6 (πœ‘ β†’ Fun ((,) ∘ 𝐹))
171170adantr 479 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Fun ((,) ∘ 𝐹))
1725fdmd 6727 . . . . . . . 8 (πœ‘ β†’ dom ((,) ∘ 𝐹) = β„•)
173172eqcomd 2731 . . . . . . 7 (πœ‘ β†’ β„• = dom ((,) ∘ 𝐹))
174173adantr 479 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ β„• = dom ((,) ∘ 𝐹))
175129, 174eleqtrd 2827 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ dom ((,) ∘ 𝐹))
176 fvco 6989 . . . . 5 ((Fun ((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) β†’ ((vol ∘ ((,) ∘ 𝐹))β€˜π‘›) = (volβ€˜(((,) ∘ 𝐹)β€˜π‘›)))
177171, 175, 176syl2anc 582 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((vol ∘ ((,) ∘ 𝐹))β€˜π‘›) = (volβ€˜(((,) ∘ 𝐹)β€˜π‘›)))
178 fnfun 6649 . . . . . . 7 (((,) ∘ 𝐺) Fn β„• β†’ Fun ((,) ∘ 𝐺))
17931, 178syl 17 . . . . . 6 (πœ‘ β†’ Fun ((,) ∘ 𝐺))
180179adantr 479 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Fun ((,) ∘ 𝐺))
18130fdmd 6727 . . . . . . . 8 (πœ‘ β†’ dom ((,) ∘ 𝐺) = β„•)
182181eqcomd 2731 . . . . . . 7 (πœ‘ β†’ β„• = dom ((,) ∘ 𝐺))
183182adantr 479 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ β„• = dom ((,) ∘ 𝐺))
184129, 183eleqtrd 2827 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ dom ((,) ∘ 𝐺))
185 fvco 6989 . . . . 5 ((Fun ((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) β†’ ((vol ∘ ((,) ∘ 𝐺))β€˜π‘›) = (volβ€˜(((,) ∘ 𝐺)β€˜π‘›)))
186180, 184, 185syl2anc 582 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((vol ∘ ((,) ∘ 𝐺))β€˜π‘›) = (volβ€˜(((,) ∘ 𝐺)β€˜π‘›)))
187168, 177, 1863eqtr4d 2775 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((vol ∘ ((,) ∘ 𝐹))β€˜π‘›) = ((vol ∘ ((,) ∘ 𝐺))β€˜π‘›))
188144, 163, 187eqfnfvd 7036 . 2 (πœ‘ β†’ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺)))
189125, 188jca 510 1 (πœ‘ β†’ (βˆͺ ran ((,) ∘ 𝐹) = βˆͺ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  βˆ€wral 3051  {crab 3419  Vcvv 3463   βˆ– cdif 3938   βˆͺ cun 3939   βŠ† wss 3941  βˆ…c0 4319  ifcif 4525  π’« cpw 4599  βŸ¨cop 4631  βˆͺ cuni 4904  βˆͺ ciun 4992   class class class wbr 5144   ↦ cmpt 5227   Γ— cxp 5671  dom cdm 5673  ran crn 5674   ∘ ccom 5677  Fun wfun 6537   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7413  1st c1st 7985  2nd c2nd 7986  β„cr 11132  0cc0 11133  +∞cpnf 11270  β„*cxr 11272   < clt 11273   ≀ cle 11274  β„•cn 12237  (,)cioo 13351  [,]cicc 13354  volcvol 25405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-om 7866  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-map 8840  df-pm 8841  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-sup 9460  df-inf 9461  df-oi 9528  df-dju 9919  df-card 9957  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-n0 12498  df-z 12584  df-uz 12848  df-q 12958  df-rp 13002  df-xadd 13120  df-ioo 13355  df-ico 13357  df-icc 13358  df-fz 13512  df-fzo 13655  df-fl 13784  df-seq 13994  df-exp 14054  df-hash 14317  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-clim 15459  df-rlim 15460  df-sum 15660  df-xmet 21271  df-met 21272  df-ovol 25406  df-vol 25407
This theorem is referenced by:  ovolval4lem2  46097
  Copyright terms: Public domain W3C validator