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 ffvelcdmda 
 |-  ( ( 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 ) ) ) )