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
|- ( ph -> F : NN --> ( RR* X. RR* ) )
ovolval4lem1.g
|- G = ( n e. NN |-> <. ( 1st ` ( F ` n ) ) , if ( ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) , ( 1st ` ( F ` n ) ) ) >. )
ovolval4lem1.a
|- A = { n e. NN | ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) }
Assertion ovolval4lem1
|- ( ph -> ( U. ran ( (,) o. F ) = U. ran ( (,) o. G ) /\ ( vol o. ( (,) o. F ) ) = ( vol o. ( (,) o. G ) ) ) )

Proof

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