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 45960
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 13448 . . . . . . . 8 (,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ
21a1i 11 . . . . . . 7 (πœ‘ β†’ (,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ)
3 ovolval4lem1.f . . . . . . 7 (πœ‘ β†’ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*))
4 fco 6741 . . . . . . 7 (((,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ ∧ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*)) β†’ ((,) ∘ 𝐹):β„•βŸΆπ’« ℝ)
52, 3, 4syl2anc 583 . . . . . 6 (πœ‘ β†’ ((,) ∘ 𝐹):β„•βŸΆπ’« ℝ)
65ffnd 6717 . . . . 5 (πœ‘ β†’ ((,) ∘ 𝐹) Fn β„•)
7 fniunfv 7251 . . . . 5 (((,) ∘ 𝐹) Fn β„• β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) = βˆͺ ran ((,) ∘ 𝐹))
86, 7syl 17 . . . 4 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) = βˆͺ ran ((,) ∘ 𝐹))
98eqcomd 2733 . . 3 (πœ‘ β†’ βˆͺ ran ((,) ∘ 𝐹) = βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›))
10 ovolval4lem1.a . . . . . . . . 9 𝐴 = {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))}
11 ssrab2 4073 . . . . . . . . 9 {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))} βŠ† β„•
1210, 11eqsstri 4012 . . . . . . . 8 𝐴 βŠ† β„•
13 undif 4477 . . . . . . . 8 (𝐴 βŠ† β„• ↔ (𝐴 βˆͺ (β„• βˆ– 𝐴)) = β„•)
1412, 13mpbi 229 . . . . . . 7 (𝐴 βˆͺ (β„• βˆ– 𝐴)) = β„•
1514eqcomi 2736 . . . . . 6 β„• = (𝐴 βˆͺ (β„• βˆ– 𝐴))
1615iuneq1i 44374 . . . . 5 βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) = βˆͺ 𝑛 ∈ (𝐴 βˆͺ (β„• βˆ– 𝐴))(((,) ∘ 𝐹)β€˜π‘›)
17 iunxun 5091 . . . . 5 βˆͺ 𝑛 ∈ (𝐴 βˆͺ (β„• βˆ– 𝐴))(((,) ∘ 𝐹)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›))
1816, 17eqtri 2755 . . . 4 βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›))
1918a1i 11 . . 3 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›)))
203ffvelcdmda 7088 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ (ℝ* Γ— ℝ*))
21 xp1st 8019 . . . . . . . . . . 11 ((πΉβ€˜π‘›) ∈ (ℝ* Γ— ℝ*) β†’ (1st β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
2220, 21syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (1st β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
23 xp2nd 8020 . . . . . . . . . . . 12 ((πΉβ€˜π‘›) ∈ (ℝ* Γ— ℝ*) β†’ (2nd β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
2420, 23syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (2nd β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
2524, 22ifcld 4570 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))) ∈ ℝ*)
2622, 25opelxpd 5711 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩ ∈ (ℝ* Γ— ℝ*))
27 ovolval4lem1.g . . . . . . . . 9 𝐺 = (𝑛 ∈ β„• ↦ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩)
2826, 27fmptd 7118 . . . . . . . 8 (πœ‘ β†’ 𝐺:β„•βŸΆ(ℝ* Γ— ℝ*))
29 fco 6741 . . . . . . . 8 (((,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ ∧ 𝐺:β„•βŸΆ(ℝ* Γ— ℝ*)) β†’ ((,) ∘ 𝐺):β„•βŸΆπ’« ℝ)
302, 28, 29syl2anc 583 . . . . . . 7 (πœ‘ β†’ ((,) ∘ 𝐺):β„•βŸΆπ’« ℝ)
3130ffnd 6717 . . . . . 6 (πœ‘ β†’ ((,) ∘ 𝐺) Fn β„•)
32 fniunfv 7251 . . . . . 6 (((,) ∘ 𝐺) Fn β„• β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) = βˆͺ ran ((,) ∘ 𝐺))
3331, 32syl 17 . . . . 5 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) = βˆͺ ran ((,) ∘ 𝐺))
3433eqcomd 2733 . . . 4 (πœ‘ β†’ βˆͺ ran ((,) ∘ 𝐺) = βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›))
3515iuneq1i 44374 . . . . . 6 βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) = βˆͺ 𝑛 ∈ (𝐴 βˆͺ (β„• βˆ– 𝐴))(((,) ∘ 𝐺)β€˜π‘›)
36 iunxun 5091 . . . . . 6 βˆͺ 𝑛 ∈ (𝐴 βˆͺ (β„• βˆ– 𝐴))(((,) ∘ 𝐺)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›))
3735, 36eqtri 2755 . . . . 5 βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›))
3837a1i 11 . . . 4 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›)))
3928adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ 𝐺:β„•βŸΆ(ℝ* Γ— ℝ*))
4012sseli 3974 . . . . . . . . 9 (𝑛 ∈ 𝐴 β†’ 𝑛 ∈ β„•)
4140adantl 481 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ 𝑛 ∈ β„•)
42 fvco3 6991 . . . . . . . 8 ((𝐺:β„•βŸΆ(ℝ* Γ— ℝ*) ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐺)β€˜π‘›) = ((,)β€˜(πΊβ€˜π‘›)))
4339, 41, 42syl2anc 583 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐺)β€˜π‘›) = ((,)β€˜(πΊβ€˜π‘›)))
443adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*))
45 fvco3 6991 . . . . . . . . 9 ((𝐹:β„•βŸΆ(ℝ* Γ— ℝ*) ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((,)β€˜(πΉβ€˜π‘›)))
4644, 41, 45syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((,)β€˜(πΉβ€˜π‘›)))
47 simpl 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ πœ‘)
48 1st2nd2 8026 . . . . . . . . . . . 12 ((πΉβ€˜π‘›) ∈ (ℝ* Γ— ℝ*) β†’ (πΉβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
4920, 48syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
5047, 41, 49syl2anc 583 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (πΉβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
5127a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐺 = (𝑛 ∈ β„• ↦ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩))
5226elexd 3490 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩ ∈ V)
5351, 52fvmpt2d 7012 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΊβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩)
5447, 41, 53syl2anc 583 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (πΊβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩)
5510eleq2i 2820 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))})
5655biimpi 215 . . . . . . . . . . . . . . . 16 (𝑛 ∈ 𝐴 β†’ 𝑛 ∈ {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))})
57 rabid 3447 . . . . . . . . . . . . . . . 16 (𝑛 ∈ {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))} ↔ (𝑛 ∈ β„• ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))))
5856, 57sylib 217 . . . . . . . . . . . . . . 15 (𝑛 ∈ 𝐴 β†’ (𝑛 ∈ β„• ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))))
5958simprd 495 . . . . . . . . . . . . . 14 (𝑛 ∈ 𝐴 β†’ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)))
6059adantl 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)))
6160iftrued 4532 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))) = (2nd β€˜(πΉβ€˜π‘›)))
6261opeq2d 4876 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩ = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
63 eqidd 2728 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩ = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
6454, 62, 633eqtrd 2771 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (πΊβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
6550, 64eqtr4d 2770 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (πΉβ€˜π‘›) = (πΊβ€˜π‘›))
6665fveq2d 6895 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ ((,)β€˜(πΉβ€˜π‘›)) = ((,)β€˜(πΊβ€˜π‘›)))
6746, 66eqtrd 2767 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((,)β€˜(πΊβ€˜π‘›)))
6843, 67eqtr4d 2770 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐺)β€˜π‘›) = (((,) ∘ 𝐹)β€˜π‘›))
6968iuneq2dv 5015 . . . . 5 (πœ‘ β†’ βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)β€˜π‘›) = βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›))
7028adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ 𝐺:β„•βŸΆ(ℝ* Γ— ℝ*))
71 eldifi 4122 . . . . . . . . . . 11 (𝑛 ∈ (β„• βˆ– 𝐴) β†’ 𝑛 ∈ β„•)
7271adantl 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ 𝑛 ∈ β„•)
7370, 72, 42syl2anc 583 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐺)β€˜π‘›) = ((,)β€˜(πΊβ€˜π‘›)))
74 simpl 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ πœ‘)
7574, 72, 53syl2anc 583 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (πΊβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩)
7671anim1i 614 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (β„• βˆ– 𝐴) ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))) β†’ (𝑛 ∈ β„• ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))))
7776, 57sylibr 233 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (β„• βˆ– 𝐴) ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))) β†’ 𝑛 ∈ {𝑛 ∈ β„• ∣ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))})
7877, 55sylibr 233 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (β„• βˆ– 𝐴) ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))) β†’ 𝑛 ∈ 𝐴)
7978adantll 713 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))) β†’ 𝑛 ∈ 𝐴)
80 eldifn 4123 . . . . . . . . . . . . . . 15 (𝑛 ∈ (β„• βˆ– 𝐴) β†’ Β¬ 𝑛 ∈ 𝐴)
8180ad2antlr 726 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›))) β†’ Β¬ 𝑛 ∈ 𝐴)
8279, 81pm2.65da 816 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ Β¬ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)))
8382iffalsed 4535 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))) = (1st β€˜(πΉβ€˜π‘›)))
8483opeq2d 4876 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ⟨(1st β€˜(πΉβ€˜π‘›)), if((1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›)))⟩ = ⟨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩)
8575, 84eqtrd 2767 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (πΊβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩)
8685fveq2d 6895 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((,)β€˜(πΊβ€˜π‘›)) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩))
87 iooid 13376 . . . . . . . . . . . 12 ((1st β€˜(πΉβ€˜π‘›))(,)(1st β€˜(πΉβ€˜π‘›))) = βˆ…
8887eqcomi 2736 . . . . . . . . . . 11 βˆ… = ((1st β€˜(πΉβ€˜π‘›))(,)(1st β€˜(πΉβ€˜π‘›)))
89 df-ov 7417 . . . . . . . . . . 11 ((1st β€˜(πΉβ€˜π‘›))(,)(1st β€˜(πΉβ€˜π‘›))) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩)
9088, 89eqtr2i 2756 . . . . . . . . . 10 ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩) = βˆ…
9190a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (1st β€˜(πΉβ€˜π‘›))⟩) = βˆ…)
9273, 86, 913eqtrd 2771 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐺)β€˜π‘›) = βˆ…)
9392iuneq2dv 5015 . . . . . . 7 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›) = βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)βˆ…)
94 iun0 5059 . . . . . . . 8 βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)βˆ… = βˆ…
9594a1i 11 . . . . . . 7 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)βˆ… = βˆ…)
9693, 95eqtrd 2767 . . . . . 6 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›) = βˆ…)
9774, 3syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*))
9897, 72, 45syl2anc 583 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((,)β€˜(πΉβ€˜π‘›)))
9974, 72, 49syl2anc 583 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (πΉβ€˜π‘›) = ⟨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
10099fveq2d 6895 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((,)β€˜(πΉβ€˜π‘›)) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩))
101 df-ov 7417 . . . . . . . . . . 11 ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩)
102101a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩))
103 simplr 768 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ 𝑛 ∈ (β„• βˆ– 𝐴))
10472, 22syldan 590 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (1st β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
105104adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ (1st β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
10672, 24syldan 590 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (2nd β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
107106adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ (2nd β€˜(πΉβ€˜π‘›)) ∈ ℝ*)
108 simpr 484 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›)))
109105, 107xrltnled 44668 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ ((1st β€˜(πΉβ€˜π‘›)) < (2nd β€˜(πΉβ€˜π‘›)) ↔ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))))
110108, 109mpbird 257 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ (1st β€˜(πΉβ€˜π‘›)) < (2nd β€˜(πΉβ€˜π‘›)))
111105, 107, 110xrltled 13153 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ (1st β€˜(πΉβ€˜π‘›)) ≀ (2nd β€˜(πΉβ€˜π‘›)))
112103, 111, 78syl2anc 583 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ 𝑛 ∈ 𝐴)
11380ad2antlr 726 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) ∧ Β¬ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))) β†’ Β¬ 𝑛 ∈ 𝐴)
114112, 113condan 817 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›)))
115 ioo0 13373 . . . . . . . . . . . 12 (((1st β€˜(πΉβ€˜π‘›)) ∈ ℝ* ∧ (2nd β€˜(πΉβ€˜π‘›)) ∈ ℝ*) β†’ (((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) = βˆ… ↔ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))))
116104, 106, 115syl2anc 583 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) = βˆ… ↔ (2nd β€˜(πΉβ€˜π‘›)) ≀ (1st β€˜(πΉβ€˜π‘›))))
117114, 116mpbird 257 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) = βˆ…)
118102, 117eqtr3d 2769 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩) = βˆ…)
11998, 100, 1183eqtrd 2771 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐹)β€˜π‘›) = βˆ…)
120119iuneq2dv 5015 . . . . . . 7 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›) = βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)βˆ…)
121120, 95eqtrd 2767 . . . . . 6 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›) = βˆ…)
12296, 121eqtr4d 2770 . . . . 5 (πœ‘ β†’ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›) = βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›))
12369, 122uneq12d 4160 . . . 4 (πœ‘ β†’ (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐺)β€˜π‘›)) = (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›)))
12434, 38, 1233eqtrrd 2772 . . 3 (πœ‘ β†’ (βˆͺ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)β€˜π‘›) βˆͺ βˆͺ 𝑛 ∈ (β„• βˆ– 𝐴)(((,) ∘ 𝐹)β€˜π‘›)) = βˆͺ ran ((,) ∘ 𝐺))
1259, 19, 1243eqtrd 2771 . 2 (πœ‘ β†’ βˆͺ ran ((,) ∘ 𝐹) = βˆͺ ran ((,) ∘ 𝐺))
126 volf 25445 . . . . . 6 vol:dom vol⟢(0[,]+∞)
127126a1i 11 . . . . 5 (πœ‘ β†’ vol:dom vol⟢(0[,]+∞))
1283adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐹:β„•βŸΆ(ℝ* Γ— ℝ*))
129 simpr 484 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
130128, 129, 45syl2anc 583 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((,)β€˜(πΉβ€˜π‘›)))
13149fveq2d 6895 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((,)β€˜(πΉβ€˜π‘›)) = ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩))
132101eqcomi 2736 . . . . . . . . . . 11 ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩) = ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›)))
133132a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((,)β€˜βŸ¨(1st β€˜(πΉβ€˜π‘›)), (2nd β€˜(πΉβ€˜π‘›))⟩) = ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))))
134130, 131, 1333eqtrd 2771 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐹)β€˜π‘›) = ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))))
135 ioombl 25481 . . . . . . . . . 10 ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) ∈ dom vol
136135a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((1st β€˜(πΉβ€˜π‘›))(,)(2nd β€˜(πΉβ€˜π‘›))) ∈ dom vol)
137134, 136eqeltrd 2828 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐹)β€˜π‘›) ∈ dom vol)
138137ralrimiva 3141 . . . . . . 7 (πœ‘ β†’ βˆ€π‘› ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) ∈ dom vol)
1396, 138jca 511 . . . . . 6 (πœ‘ β†’ (((,) ∘ 𝐹) Fn β„• ∧ βˆ€π‘› ∈ β„• (((,) ∘ 𝐹)β€˜π‘›) ∈ dom vol))
140 ffnfv 7123 . . . . . 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 583 . . . 4 (πœ‘ β†’ (vol ∘ ((,) ∘ 𝐹)):β„•βŸΆ(0[,]+∞))
144143ffnd 6717 . . 3 (πœ‘ β†’ (vol ∘ ((,) ∘ 𝐹)) Fn β„•)
14568adantlr 714 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐺)β€˜π‘›) = (((,) ∘ 𝐹)β€˜π‘›))
146137adantr 480 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐹)β€˜π‘›) ∈ dom vol)
147145, 146eqeltrd 2828 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol)
148 simpll 766 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ Β¬ 𝑛 ∈ 𝐴) β†’ πœ‘)
149 eldif 3954 . . . . . . . . . . . . 13 (𝑛 ∈ (β„• βˆ– 𝐴) ↔ (𝑛 ∈ β„• ∧ Β¬ 𝑛 ∈ 𝐴))
150149bicomi 223 . . . . . . . . . . . 12 ((𝑛 ∈ β„• ∧ Β¬ 𝑛 ∈ 𝐴) ↔ 𝑛 ∈ (β„• βˆ– 𝐴))
151150biimpi 215 . . . . . . . . . . 11 ((𝑛 ∈ β„• ∧ Β¬ 𝑛 ∈ 𝐴) β†’ 𝑛 ∈ (β„• βˆ– 𝐴))
152151adantll 713 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ Β¬ 𝑛 ∈ 𝐴) β†’ 𝑛 ∈ (β„• βˆ– 𝐴))
153117, 135eqeltrrdi 2837 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ βˆ… ∈ dom vol)
15492, 153eqeltrd 2828 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol)
155148, 152, 154syl2anc 583 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ Β¬ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol)
156147, 155pm2.61dan 812 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol)
157156ralrimiva 3141 . . . . . . 7 (πœ‘ β†’ βˆ€π‘› ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol)
15831, 157jca 511 . . . . . 6 (πœ‘ β†’ (((,) ∘ 𝐺) Fn β„• ∧ βˆ€π‘› ∈ β„• (((,) ∘ 𝐺)β€˜π‘›) ∈ dom vol))
159 ffnfv 7123 . . . . . 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 583 . . . 4 (πœ‘ β†’ (vol ∘ ((,) ∘ 𝐺)):β„•βŸΆ(0[,]+∞))
163162ffnd 6717 . . 3 (πœ‘ β†’ (vol ∘ ((,) ∘ 𝐺)) Fn β„•)
164145eqcomd 2733 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐹)β€˜π‘›) = (((,) ∘ 𝐺)β€˜π‘›))
165119, 92eqtr4d 2770 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (β„• βˆ– 𝐴)) β†’ (((,) ∘ 𝐹)β€˜π‘›) = (((,) ∘ 𝐺)β€˜π‘›))
166148, 152, 165syl2anc 583 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ Β¬ 𝑛 ∈ 𝐴) β†’ (((,) ∘ 𝐹)β€˜π‘›) = (((,) ∘ 𝐺)β€˜π‘›))
167164, 166pm2.61dan 812 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (((,) ∘ 𝐹)β€˜π‘›) = (((,) ∘ 𝐺)β€˜π‘›))
168167fveq2d 6895 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (volβ€˜(((,) ∘ 𝐹)β€˜π‘›)) = (volβ€˜(((,) ∘ 𝐺)β€˜π‘›)))
169 fnfun 6648 . . . . . . 7 (((,) ∘ 𝐹) Fn β„• β†’ Fun ((,) ∘ 𝐹))
1706, 169syl 17 . . . . . 6 (πœ‘ β†’ Fun ((,) ∘ 𝐹))
171170adantr 480 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Fun ((,) ∘ 𝐹))
1725fdmd 6727 . . . . . . . 8 (πœ‘ β†’ dom ((,) ∘ 𝐹) = β„•)
173172eqcomd 2733 . . . . . . 7 (πœ‘ β†’ β„• = dom ((,) ∘ 𝐹))
174173adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ β„• = dom ((,) ∘ 𝐹))
175129, 174eleqtrd 2830 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ dom ((,) ∘ 𝐹))
176 fvco 6990 . . . . 5 ((Fun ((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) β†’ ((vol ∘ ((,) ∘ 𝐹))β€˜π‘›) = (volβ€˜(((,) ∘ 𝐹)β€˜π‘›)))
177171, 175, 176syl2anc 583 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((vol ∘ ((,) ∘ 𝐹))β€˜π‘›) = (volβ€˜(((,) ∘ 𝐹)β€˜π‘›)))
178 fnfun 6648 . . . . . . 7 (((,) ∘ 𝐺) Fn β„• β†’ Fun ((,) ∘ 𝐺))
17931, 178syl 17 . . . . . 6 (πœ‘ β†’ Fun ((,) ∘ 𝐺))
180179adantr 480 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ Fun ((,) ∘ 𝐺))
18130fdmd 6727 . . . . . . . 8 (πœ‘ β†’ dom ((,) ∘ 𝐺) = β„•)
182181eqcomd 2733 . . . . . . 7 (πœ‘ β†’ β„• = dom ((,) ∘ 𝐺))
183182adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ β„• = dom ((,) ∘ 𝐺))
184129, 183eleqtrd 2830 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ dom ((,) ∘ 𝐺))
185 fvco 6990 . . . . 5 ((Fun ((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) β†’ ((vol ∘ ((,) ∘ 𝐺))β€˜π‘›) = (volβ€˜(((,) ∘ 𝐺)β€˜π‘›)))
186180, 184, 185syl2anc 583 . . . 4 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((vol ∘ ((,) ∘ 𝐺))β€˜π‘›) = (volβ€˜(((,) ∘ 𝐺)β€˜π‘›)))
187168, 177, 1863eqtr4d 2777 . . 3 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((vol ∘ ((,) ∘ 𝐹))β€˜π‘›) = ((vol ∘ ((,) ∘ 𝐺))β€˜π‘›))
188144, 163, 187eqfnfvd 7037 . 2 (πœ‘ β†’ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺)))
189125, 188jca 511 1 (πœ‘ β†’ (βˆͺ ran ((,) ∘ 𝐹) = βˆͺ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099  βˆ€wral 3056  {crab 3427  Vcvv 3469   βˆ– cdif 3941   βˆͺ cun 3942   βŠ† wss 3944  βˆ…c0 4318  ifcif 4524  π’« cpw 4598  βŸ¨cop 4630  βˆͺ cuni 4903  βˆͺ ciun 4991   class class class wbr 5142   ↦ cmpt 5225   Γ— cxp 5670  dom cdm 5672  ran crn 5673   ∘ ccom 5676  Fun wfun 6536   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414  1st c1st 7985  2nd c2nd 7986  β„cr 11129  0cc0 11130  +∞cpnf 11267  β„*cxr 11269   < clt 11270   ≀ cle 11271  β„•cn 12234  (,)cioo 13348  [,]cicc 13351  volcvol 25379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  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 8838  df-pm 8839  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9457  df-inf 9458  df-oi 9525  df-dju 9916  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-z 12581  df-uz 12845  df-q 12955  df-rp 12999  df-xadd 13117  df-ioo 13352  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-fl 13781  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-clim 15456  df-rlim 15457  df-sum 15657  df-xmet 21259  df-met 21260  df-ovol 25380  df-vol 25381
This theorem is referenced by:  ovolval4lem2  45961
  Copyright terms: Public domain W3C validator