Metamath Proof Explorer


Theorem ovolval4lem1

Description: |- ( ( ph /\ n e. A ) -> ( ( (,) o. G ) n ) = ( ( (,) o. F ) n ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval4lem1.f ( 𝜑𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
ovolval4lem1.g 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ⟩ )
ovolval4lem1.a 𝐴 = { 𝑛 ∈ ℕ ∣ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) }
Assertion ovolval4lem1 ( 𝜑 → ( ran ( (,) ∘ 𝐹 ) = ran ( (,) ∘ 𝐺 ) ∧ ( vol ∘ ( (,) ∘ 𝐹 ) ) = ( vol ∘ ( (,) ∘ 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 ovolval4lem1.f ( 𝜑𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
2 ovolval4lem1.g 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ⟩ )
3 ovolval4lem1.a 𝐴 = { 𝑛 ∈ ℕ ∣ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) }
4 ioof (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
5 4 a1i ( 𝜑 → (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ )
6 fco ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
7 5 1 6 syl2anc ( 𝜑 → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
8 7 ffnd ( 𝜑 → ( (,) ∘ 𝐹 ) Fn ℕ )
9 fniunfv ( ( (,) ∘ 𝐹 ) Fn ℕ → 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ran ( (,) ∘ 𝐹 ) )
10 8 9 syl ( 𝜑 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ran ( (,) ∘ 𝐹 ) )
11 10 eqcomd ( 𝜑 ran ( (,) ∘ 𝐹 ) = 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) )
12 ssrab2 { 𝑛 ∈ ℕ ∣ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) } ⊆ ℕ
13 3 12 eqsstri 𝐴 ⊆ ℕ
14 undif ( 𝐴 ⊆ ℕ ↔ ( 𝐴 ∪ ( ℕ ∖ 𝐴 ) ) = ℕ )
15 13 14 mpbi ( 𝐴 ∪ ( ℕ ∖ 𝐴 ) ) = ℕ
16 15 eqcomi ℕ = ( 𝐴 ∪ ( ℕ ∖ 𝐴 ) )
17 16 iuneq1i 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = 𝑛 ∈ ( 𝐴 ∪ ( ℕ ∖ 𝐴 ) ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 )
18 iunxun 𝑛 ∈ ( 𝐴 ∪ ( ℕ ∖ 𝐴 ) ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( 𝑛𝐴 ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∪ 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) )
19 17 18 eqtri 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( 𝑛𝐴 ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∪ 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) )
20 19 a1i ( 𝜑 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( 𝑛𝐴 ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∪ 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ) )
21 1 ffvelrnda ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ∈ ( ℝ* × ℝ* ) )
22 xp1st ( ( 𝐹𝑛 ) ∈ ( ℝ* × ℝ* ) → ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ* )
23 21 22 syl ( ( 𝜑𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ* )
24 xp2nd ( ( 𝐹𝑛 ) ∈ ( ℝ* × ℝ* ) → ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ* )
25 21 24 syl ( ( 𝜑𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ* )
26 25 23 ifcld ( ( 𝜑𝑛 ∈ ℕ ) → if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ∈ ℝ* )
27 23 26 opelxpd ( ( 𝜑𝑛 ∈ ℕ ) → ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ⟩ ∈ ( ℝ* × ℝ* ) )
28 27 2 fmptd ( 𝜑𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
29 fco ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ )
30 5 28 29 syl2anc ( 𝜑 → ( (,) ∘ 𝐺 ) : ℕ ⟶ 𝒫 ℝ )
31 30 ffnd ( 𝜑 → ( (,) ∘ 𝐺 ) Fn ℕ )
32 fniunfv ( ( (,) ∘ 𝐺 ) Fn ℕ → 𝑛 ∈ ℕ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ran ( (,) ∘ 𝐺 ) )
33 31 32 syl ( 𝜑 𝑛 ∈ ℕ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ran ( (,) ∘ 𝐺 ) )
34 33 eqcomd ( 𝜑 ran ( (,) ∘ 𝐺 ) = 𝑛 ∈ ℕ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) )
35 16 iuneq1i 𝑛 ∈ ℕ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = 𝑛 ∈ ( 𝐴 ∪ ( ℕ ∖ 𝐴 ) ) ( ( (,) ∘ 𝐺 ) ‘ 𝑛 )
36 iunxun 𝑛 ∈ ( 𝐴 ∪ ( ℕ ∖ 𝐴 ) ) ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ( 𝑛𝐴 ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∪ 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) )
37 35 36 eqtri 𝑛 ∈ ℕ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ( 𝑛𝐴 ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∪ 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) )
38 37 a1i ( 𝜑 𝑛 ∈ ℕ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ( 𝑛𝐴 ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∪ 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ) )
39 28 adantr ( ( 𝜑𝑛𝐴 ) → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
40 13 sseli ( 𝑛𝐴𝑛 ∈ ℕ )
41 40 adantl ( ( 𝜑𝑛𝐴 ) → 𝑛 ∈ ℕ )
42 fvco3 ( ( 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) ∧ 𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐺𝑛 ) ) )
43 39 41 42 syl2anc ( ( 𝜑𝑛𝐴 ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐺𝑛 ) ) )
44 1 adantr ( ( 𝜑𝑛𝐴 ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
45 fvco3 ( ( 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ∧ 𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐹𝑛 ) ) )
46 44 41 45 syl2anc ( ( 𝜑𝑛𝐴 ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐹𝑛 ) ) )
47 simpl ( ( 𝜑𝑛𝐴 ) → 𝜑 )
48 1st2nd2 ( ( 𝐹𝑛 ) ∈ ( ℝ* × ℝ* ) → ( 𝐹𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
49 21 48 syl ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
50 47 41 49 syl2anc ( ( 𝜑𝑛𝐴 ) → ( 𝐹𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
51 2 a1i ( 𝜑𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ⟩ ) )
52 27 elexd ( ( 𝜑𝑛 ∈ ℕ ) → ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ⟩ ∈ V )
53 51 52 fvmpt2d ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐺𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ⟩ )
54 47 41 53 syl2anc ( ( 𝜑𝑛𝐴 ) → ( 𝐺𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ⟩ )
55 3 eleq2i ( 𝑛𝐴𝑛 ∈ { 𝑛 ∈ ℕ ∣ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) } )
56 55 biimpi ( 𝑛𝐴𝑛 ∈ { 𝑛 ∈ ℕ ∣ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) } )
57 rabid ( 𝑛 ∈ { 𝑛 ∈ ℕ ∣ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) } ↔ ( 𝑛 ∈ ℕ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
58 56 57 sylib ( 𝑛𝐴 → ( 𝑛 ∈ ℕ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
59 58 simprd ( 𝑛𝐴 → ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) )
60 59 adantl ( ( 𝜑𝑛𝐴 ) → ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) )
61 60 iftrued ( ( 𝜑𝑛𝐴 ) → if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) = ( 2nd ‘ ( 𝐹𝑛 ) ) )
62 61 opeq2d ( ( 𝜑𝑛𝐴 ) → ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ⟩ = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
63 eqidd ( ( 𝜑𝑛𝐴 ) → ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
64 54 62 63 3eqtrd ( ( 𝜑𝑛𝐴 ) → ( 𝐺𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
65 50 64 eqtr4d ( ( 𝜑𝑛𝐴 ) → ( 𝐹𝑛 ) = ( 𝐺𝑛 ) )
66 65 fveq2d ( ( 𝜑𝑛𝐴 ) → ( (,) ‘ ( 𝐹𝑛 ) ) = ( (,) ‘ ( 𝐺𝑛 ) ) )
67 46 66 eqtrd ( ( 𝜑𝑛𝐴 ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐺𝑛 ) ) )
68 43 67 eqtr4d ( ( 𝜑𝑛𝐴 ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) )
69 68 iuneq2dv ( 𝜑 𝑛𝐴 ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = 𝑛𝐴 ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) )
70 28 adantr ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → 𝐺 : ℕ ⟶ ( ℝ* × ℝ* ) )
71 eldifi ( 𝑛 ∈ ( ℕ ∖ 𝐴 ) → 𝑛 ∈ ℕ )
72 71 adantl ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → 𝑛 ∈ ℕ )
73 70 72 42 syl2anc ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐺𝑛 ) ) )
74 simpl ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → 𝜑 )
75 74 72 53 syl2anc ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( 𝐺𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ⟩ )
76 71 anim1i ( ( 𝑛 ∈ ( ℕ ∖ 𝐴 ) ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) → ( 𝑛 ∈ ℕ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
77 76 57 sylibr ( ( 𝑛 ∈ ( ℕ ∖ 𝐴 ) ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) → 𝑛 ∈ { 𝑛 ∈ ℕ ∣ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) } )
78 77 55 sylibr ( ( 𝑛 ∈ ( ℕ ∖ 𝐴 ) ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) → 𝑛𝐴 )
79 78 adantll ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) → 𝑛𝐴 )
80 eldifn ( 𝑛 ∈ ( ℕ ∖ 𝐴 ) → ¬ 𝑛𝐴 )
81 80 ad2antlr ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) → ¬ 𝑛𝐴 )
82 79 81 pm2.65da ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ¬ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) )
83 82 iffalsed ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) = ( 1st ‘ ( 𝐹𝑛 ) ) )
84 83 opeq2d ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , if ( ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ) ⟩ = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ⟩ )
85 75 84 eqtrd ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( 𝐺𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ⟩ )
86 85 fveq2d ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( (,) ‘ ( 𝐺𝑛 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ⟩ ) )
87 iooid ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 1st ‘ ( 𝐹𝑛 ) ) ) = ∅
88 87 eqcomi ∅ = ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 1st ‘ ( 𝐹𝑛 ) ) )
89 df-ov ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 1st ‘ ( 𝐹𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ⟩ )
90 88 89 eqtr2i ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ⟩ ) = ∅
91 90 a1i ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 1st ‘ ( 𝐹𝑛 ) ) ⟩ ) = ∅ )
92 73 86 91 3eqtrd ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ∅ )
93 92 iuneq2dv ( 𝜑 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = 𝑛 ∈ ( ℕ ∖ 𝐴 ) ∅ )
94 iun0 𝑛 ∈ ( ℕ ∖ 𝐴 ) ∅ = ∅
95 94 a1i ( 𝜑 𝑛 ∈ ( ℕ ∖ 𝐴 ) ∅ = ∅ )
96 93 95 eqtrd ( 𝜑 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ∅ )
97 74 1 syl ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
98 97 72 45 syl2anc ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐹𝑛 ) ) )
99 74 72 49 syl2anc ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( 𝐹𝑛 ) = ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
100 99 fveq2d ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( (,) ‘ ( 𝐹𝑛 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ ) )
101 df-ov ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 2nd ‘ ( 𝐹𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ )
102 101 a1i ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 2nd ‘ ( 𝐹𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ ) )
103 simplr ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) → 𝑛 ∈ ( ℕ ∖ 𝐴 ) )
104 72 23 syldan ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ* )
105 104 adantr ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) → ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ* )
106 72 25 syldan ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ* )
107 106 adantr ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) → ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ* )
108 simpr ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) → ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) )
109 105 107 xrltnled ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) < ( 2nd ‘ ( 𝐹𝑛 ) ) ↔ ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) )
110 108 109 mpbird ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) → ( 1st ‘ ( 𝐹𝑛 ) ) < ( 2nd ‘ ( 𝐹𝑛 ) ) )
111 105 107 110 xrltled ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) → ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) )
112 103 111 78 syl2anc ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) → 𝑛𝐴 )
113 80 ad2antlr ( ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) ∧ ¬ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) → ¬ 𝑛𝐴 )
114 112 113 condan ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) )
115 ioo0 ( ( ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ* ∧ ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ* ) → ( ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 2nd ‘ ( 𝐹𝑛 ) ) ) = ∅ ↔ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) )
116 104 106 115 syl2anc ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 2nd ‘ ( 𝐹𝑛 ) ) ) = ∅ ↔ ( 2nd ‘ ( 𝐹𝑛 ) ) ≤ ( 1st ‘ ( 𝐹𝑛 ) ) ) )
117 114 116 mpbird ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 2nd ‘ ( 𝐹𝑛 ) ) ) = ∅ )
118 102 117 eqtr3d ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ ) = ∅ )
119 98 100 118 3eqtrd ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ∅ )
120 119 iuneq2dv ( 𝜑 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = 𝑛 ∈ ( ℕ ∖ 𝐴 ) ∅ )
121 120 95 eqtrd ( 𝜑 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ∅ )
122 96 121 eqtr4d ( 𝜑 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) )
123 69 122 uneq12d ( 𝜑 → ( 𝑛𝐴 ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∪ 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ) = ( 𝑛𝐴 ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∪ 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ) )
124 34 38 123 3eqtrrd ( 𝜑 → ( 𝑛𝐴 ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∪ 𝑛 ∈ ( ℕ ∖ 𝐴 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ) = ran ( (,) ∘ 𝐺 ) )
125 11 20 124 3eqtrd ( 𝜑 ran ( (,) ∘ 𝐹 ) = ran ( (,) ∘ 𝐺 ) )
126 volf vol : dom vol ⟶ ( 0 [,] +∞ )
127 126 a1i ( 𝜑 → vol : dom vol ⟶ ( 0 [,] +∞ ) )
128 1 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
129 simpr ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
130 128 129 45 syl2anc ( ( 𝜑𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐹𝑛 ) ) )
131 49 fveq2d ( ( 𝜑𝑛 ∈ ℕ ) → ( (,) ‘ ( 𝐹𝑛 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ ) )
132 101 eqcomi ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ ) = ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 2nd ‘ ( 𝐹𝑛 ) ) )
133 132 a1i ( ( 𝜑𝑛 ∈ ℕ ) → ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹𝑛 ) ) , ( 2nd ‘ ( 𝐹𝑛 ) ) ⟩ ) = ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
134 130 131 133 3eqtrd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
135 ioombl ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 2nd ‘ ( 𝐹𝑛 ) ) ) ∈ dom vol
136 135 a1i ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) (,) ( 2nd ‘ ( 𝐹𝑛 ) ) ) ∈ dom vol )
137 134 136 eqeltrd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∈ dom vol )
138 137 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∈ dom vol )
139 8 138 jca ( 𝜑 → ( ( (,) ∘ 𝐹 ) Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∈ dom vol ) )
140 ffnfv ( ( (,) ∘ 𝐹 ) : ℕ ⟶ dom vol ↔ ( ( (,) ∘ 𝐹 ) Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∈ dom vol ) )
141 139 140 sylibr ( 𝜑 → ( (,) ∘ 𝐹 ) : ℕ ⟶ dom vol )
142 fco ( ( vol : dom vol ⟶ ( 0 [,] +∞ ) ∧ ( (,) ∘ 𝐹 ) : ℕ ⟶ dom vol ) → ( vol ∘ ( (,) ∘ 𝐹 ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
143 127 141 142 syl2anc ( 𝜑 → ( vol ∘ ( (,) ∘ 𝐹 ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
144 143 ffnd ( 𝜑 → ( vol ∘ ( (,) ∘ 𝐹 ) ) Fn ℕ )
145 68 adantlr ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑛𝐴 ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) )
146 137 adantr ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑛𝐴 ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∈ dom vol )
147 145 146 eqeltrd ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑛𝐴 ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∈ dom vol )
148 simpll ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ ¬ 𝑛𝐴 ) → 𝜑 )
149 eldif ( 𝑛 ∈ ( ℕ ∖ 𝐴 ) ↔ ( 𝑛 ∈ ℕ ∧ ¬ 𝑛𝐴 ) )
150 149 bicomi ( ( 𝑛 ∈ ℕ ∧ ¬ 𝑛𝐴 ) ↔ 𝑛 ∈ ( ℕ ∖ 𝐴 ) )
151 150 biimpi ( ( 𝑛 ∈ ℕ ∧ ¬ 𝑛𝐴 ) → 𝑛 ∈ ( ℕ ∖ 𝐴 ) )
152 151 adantll ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ ¬ 𝑛𝐴 ) → 𝑛 ∈ ( ℕ ∖ 𝐴 ) )
153 117 135 eqeltrrdi ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ∅ ∈ dom vol )
154 92 153 eqeltrd ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∈ dom vol )
155 148 152 154 syl2anc ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ ¬ 𝑛𝐴 ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∈ dom vol )
156 147 155 pm2.61dan ( ( 𝜑𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∈ dom vol )
157 156 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∈ dom vol )
158 31 157 jca ( 𝜑 → ( ( (,) ∘ 𝐺 ) Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∈ dom vol ) )
159 ffnfv ( ( (,) ∘ 𝐺 ) : ℕ ⟶ dom vol ↔ ( ( (,) ∘ 𝐺 ) Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ∈ dom vol ) )
160 158 159 sylibr ( 𝜑 → ( (,) ∘ 𝐺 ) : ℕ ⟶ dom vol )
161 fco ( ( vol : dom vol ⟶ ( 0 [,] +∞ ) ∧ ( (,) ∘ 𝐺 ) : ℕ ⟶ dom vol ) → ( vol ∘ ( (,) ∘ 𝐺 ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
162 127 160 161 syl2anc ( 𝜑 → ( vol ∘ ( (,) ∘ 𝐺 ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
163 162 ffnd ( 𝜑 → ( vol ∘ ( (,) ∘ 𝐺 ) ) Fn ℕ )
164 145 eqcomd ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑛𝐴 ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) )
165 119 92 eqtr4d ( ( 𝜑𝑛 ∈ ( ℕ ∖ 𝐴 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) )
166 148 152 165 syl2anc ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ ¬ 𝑛𝐴 ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) )
167 164 166 pm2.61dan ( ( 𝜑𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) )
168 167 fveq2d ( ( 𝜑𝑛 ∈ ℕ ) → ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ) = ( vol ‘ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ) )
169 fnfun ( ( (,) ∘ 𝐹 ) Fn ℕ → Fun ( (,) ∘ 𝐹 ) )
170 8 169 syl ( 𝜑 → Fun ( (,) ∘ 𝐹 ) )
171 170 adantr ( ( 𝜑𝑛 ∈ ℕ ) → Fun ( (,) ∘ 𝐹 ) )
172 7 fdmd ( 𝜑 → dom ( (,) ∘ 𝐹 ) = ℕ )
173 172 eqcomd ( 𝜑 → ℕ = dom ( (,) ∘ 𝐹 ) )
174 173 adantr ( ( 𝜑𝑛 ∈ ℕ ) → ℕ = dom ( (,) ∘ 𝐹 ) )
175 129 174 eleqtrd ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ∈ dom ( (,) ∘ 𝐹 ) )
176 fvco ( ( Fun ( (,) ∘ 𝐹 ) ∧ 𝑛 ∈ dom ( (,) ∘ 𝐹 ) ) → ( ( vol ∘ ( (,) ∘ 𝐹 ) ) ‘ 𝑛 ) = ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ) )
177 171 175 176 syl2anc ( ( 𝜑𝑛 ∈ ℕ ) → ( ( vol ∘ ( (,) ∘ 𝐹 ) ) ‘ 𝑛 ) = ( vol ‘ ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ) )
178 fnfun ( ( (,) ∘ 𝐺 ) Fn ℕ → Fun ( (,) ∘ 𝐺 ) )
179 31 178 syl ( 𝜑 → Fun ( (,) ∘ 𝐺 ) )
180 179 adantr ( ( 𝜑𝑛 ∈ ℕ ) → Fun ( (,) ∘ 𝐺 ) )
181 30 fdmd ( 𝜑 → dom ( (,) ∘ 𝐺 ) = ℕ )
182 181 eqcomd ( 𝜑 → ℕ = dom ( (,) ∘ 𝐺 ) )
183 182 adantr ( ( 𝜑𝑛 ∈ ℕ ) → ℕ = dom ( (,) ∘ 𝐺 ) )
184 129 183 eleqtrd ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ∈ dom ( (,) ∘ 𝐺 ) )
185 fvco ( ( Fun ( (,) ∘ 𝐺 ) ∧ 𝑛 ∈ dom ( (,) ∘ 𝐺 ) ) → ( ( vol ∘ ( (,) ∘ 𝐺 ) ) ‘ 𝑛 ) = ( vol ‘ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ) )
186 180 184 185 syl2anc ( ( 𝜑𝑛 ∈ ℕ ) → ( ( vol ∘ ( (,) ∘ 𝐺 ) ) ‘ 𝑛 ) = ( vol ‘ ( ( (,) ∘ 𝐺 ) ‘ 𝑛 ) ) )
187 168 177 186 3eqtr4d ( ( 𝜑𝑛 ∈ ℕ ) → ( ( vol ∘ ( (,) ∘ 𝐹 ) ) ‘ 𝑛 ) = ( ( vol ∘ ( (,) ∘ 𝐺 ) ) ‘ 𝑛 ) )
188 144 163 187 eqfnfvd ( 𝜑 → ( vol ∘ ( (,) ∘ 𝐹 ) ) = ( vol ∘ ( (,) ∘ 𝐺 ) ) )
189 125 188 jca ( 𝜑 → ( ran ( (,) ∘ 𝐹 ) = ran ( (,) ∘ 𝐺 ) ∧ ( vol ∘ ( (,) ∘ 𝐹 ) ) = ( vol ∘ ( (,) ∘ 𝐺 ) ) ) )