MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dyadmbl Structured version   Unicode version

Theorem dyadmbl 22175
Description: Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015.)
Hypotheses
Ref Expression
dyadmbl.1  |-  F  =  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)
dyadmbl.2  |-  G  =  { z  e.  A  |  A. w  e.  A  ( ( [,] `  z
)  C_  ( [,] `  w )  ->  z  =  w ) }
dyadmbl.3  |-  ( ph  ->  A  C_  ran  F )
Assertion
Ref Expression
dyadmbl  |-  ( ph  ->  U. ( [,] " A
)  e.  dom  vol )
Distinct variable groups:    x, y    z, w, ph    x, w, y, A, z    z, G   
w, F, x, y, z
Allowed substitution hints:    ph( x, y)    G( x, y, w)

Proof of Theorem dyadmbl
Dummy variables  f 
a  b  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dyadmbl.1 . . 3  |-  F  =  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)
2 dyadmbl.2 . . 3  |-  G  =  { z  e.  A  |  A. w  e.  A  ( ( [,] `  z
)  C_  ( [,] `  w )  ->  z  =  w ) }
3 dyadmbl.3 . . 3  |-  ( ph  ->  A  C_  ran  F )
41, 2, 3dyadmbllem 22174 . 2  |-  ( ph  ->  U. ( [,] " A
)  =  U. ( [,] " G ) )
5 isfinite 8060 . . . 4  |-  ( G  e.  Fin  <->  G  ~<  om )
6 iccf 11626 . . . . . 6  |-  [,] :
( RR*  X.  RR* ) --> ~P RR*
7 ffun 5715 . . . . . 6  |-  ( [,]
: ( RR*  X.  RR* )
--> ~P RR*  ->  Fun  [,] )
8 funiunfv 6135 . . . . . 6  |-  ( Fun 
[,]  ->  U_ n  e.  G  ( [,] `  n )  =  U. ( [,] " G ) )
96, 7, 8mp2b 10 . . . . 5  |-  U_ n  e.  G  ( [,] `  n )  =  U. ( [,] " G )
10 simpr 459 . . . . . 6  |-  ( (
ph  /\  G  e.  Fin )  ->  G  e. 
Fin )
11 ssrab2 3571 . . . . . . . . . . . . . . . 16  |-  { z  e.  A  |  A. w  e.  A  (
( [,] `  z
)  C_  ( [,] `  w )  ->  z  =  w ) }  C_  A
122, 11eqsstri 3519 . . . . . . . . . . . . . . 15  |-  G  C_  A
1312, 3syl5ss 3500 . . . . . . . . . . . . . 14  |-  ( ph  ->  G  C_  ran  F )
141dyadf 22166 . . . . . . . . . . . . . . . 16  |-  F :
( ZZ  X.  NN0 )
--> (  <_  i^i  ( RR  X.  RR ) )
15 frn 5719 . . . . . . . . . . . . . . . 16  |-  ( F : ( ZZ  X.  NN0 ) --> (  <_  i^i  ( RR  X.  RR ) )  ->  ran  F 
C_  (  <_  i^i  ( RR  X.  RR ) ) )
1614, 15ax-mp 5 . . . . . . . . . . . . . . 15  |-  ran  F  C_  (  <_  i^i  ( RR  X.  RR ) )
17 inss2 3705 . . . . . . . . . . . . . . 15  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR )
1816, 17sstri 3498 . . . . . . . . . . . . . 14  |-  ran  F  C_  ( RR  X.  RR )
1913, 18syl6ss 3501 . . . . . . . . . . . . 13  |-  ( ph  ->  G  C_  ( RR  X.  RR ) )
2019adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  G  e.  Fin )  ->  G  C_  ( RR  X.  RR ) )
2120sselda 3489 . . . . . . . . . . 11  |-  ( ( ( ph  /\  G  e.  Fin )  /\  n  e.  G )  ->  n  e.  ( RR  X.  RR ) )
22 1st2nd2 6810 . . . . . . . . . . 11  |-  ( n  e.  ( RR  X.  RR )  ->  n  = 
<. ( 1st `  n
) ,  ( 2nd `  n ) >. )
2321, 22syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  G  e.  Fin )  /\  n  e.  G )  ->  n  =  <. ( 1st `  n
) ,  ( 2nd `  n ) >. )
2423fveq2d 5852 . . . . . . . . 9  |-  ( ( ( ph  /\  G  e.  Fin )  /\  n  e.  G )  ->  ( [,] `  n )  =  ( [,] `  <. ( 1st `  n ) ,  ( 2nd `  n
) >. ) )
25 df-ov 6273 . . . . . . . . 9  |-  ( ( 1st `  n ) [,] ( 2nd `  n
) )  =  ( [,] `  <. ( 1st `  n ) ,  ( 2nd `  n
) >. )
2624, 25syl6eqr 2513 . . . . . . . 8  |-  ( ( ( ph  /\  G  e.  Fin )  /\  n  e.  G )  ->  ( [,] `  n )  =  ( ( 1st `  n
) [,] ( 2nd `  n ) ) )
27 xp1st 6803 . . . . . . . . . 10  |-  ( n  e.  ( RR  X.  RR )  ->  ( 1st `  n )  e.  RR )
2821, 27syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  G  e.  Fin )  /\  n  e.  G )  ->  ( 1st `  n )  e.  RR )
29 xp2nd 6804 . . . . . . . . . 10  |-  ( n  e.  ( RR  X.  RR )  ->  ( 2nd `  n )  e.  RR )
3021, 29syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  G  e.  Fin )  /\  n  e.  G )  ->  ( 2nd `  n )  e.  RR )
31 iccmbl 22142 . . . . . . . . 9  |-  ( ( ( 1st `  n
)  e.  RR  /\  ( 2nd `  n )  e.  RR )  -> 
( ( 1st `  n
) [,] ( 2nd `  n ) )  e. 
dom  vol )
3228, 30, 31syl2anc 659 . . . . . . . 8  |-  ( ( ( ph  /\  G  e.  Fin )  /\  n  e.  G )  ->  (
( 1st `  n
) [,] ( 2nd `  n ) )  e. 
dom  vol )
3326, 32eqeltrd 2542 . . . . . . 7  |-  ( ( ( ph  /\  G  e.  Fin )  /\  n  e.  G )  ->  ( [,] `  n )  e. 
dom  vol )
3433ralrimiva 2868 . . . . . 6  |-  ( (
ph  /\  G  e.  Fin )  ->  A. n  e.  G  ( [,] `  n )  e.  dom  vol )
35 finiunmbl 22120 . . . . . 6  |-  ( ( G  e.  Fin  /\  A. n  e.  G  ( [,] `  n )  e.  dom  vol )  ->  U_ n  e.  G  ( [,] `  n )  e.  dom  vol )
3610, 34, 35syl2anc 659 . . . . 5  |-  ( (
ph  /\  G  e.  Fin )  ->  U_ n  e.  G  ( [,] `  n )  e.  dom  vol )
379, 36syl5eqelr 2547 . . . 4  |-  ( (
ph  /\  G  e.  Fin )  ->  U. ( [,] " G )  e. 
dom  vol )
385, 37sylan2br 474 . . 3  |-  ( (
ph  /\  G  ~<  om )  ->  U. ( [,] " G )  e. 
dom  vol )
39 nnenom 12072 . . . . . . 7  |-  NN  ~~  om
40 ensym 7557 . . . . . . 7  |-  ( G 
~~  om  ->  om  ~~  G )
41 entr 7560 . . . . . . 7  |-  ( ( NN  ~~  om  /\  om 
~~  G )  ->  NN  ~~  G )
4239, 40, 41sylancr 661 . . . . . 6  |-  ( G 
~~  om  ->  NN  ~~  G )
43 bren 7518 . . . . . 6  |-  ( NN 
~~  G  <->  E. f 
f : NN -1-1-onto-> G )
4442, 43sylib 196 . . . . 5  |-  ( G 
~~  om  ->  E. f 
f : NN -1-1-onto-> G )
45 rnco2 5497 . . . . . . . . . 10  |-  ran  ( [,]  o.  f )  =  ( [,] " ran  f )
46 f1ofo 5805 . . . . . . . . . . . . 13  |-  ( f : NN -1-1-onto-> G  ->  f : NN -onto-> G )
4746adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  f : NN -onto-> G )
48 forn 5780 . . . . . . . . . . . 12  |-  ( f : NN -onto-> G  ->  ran  f  =  G
)
4947, 48syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  ran  f  =  G )
5049imaeq2d 5325 . . . . . . . . . 10  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  ( [,] " ran  f )  =  ( [,] " G
) )
5145, 50syl5eq 2507 . . . . . . . . 9  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  ran  ( [,]  o.  f )  =  ( [,] " G
) )
5251unieqd 4245 . . . . . . . 8  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  U. ran  ( [,]  o.  f )  =  U. ( [,] " G ) )
53 f1of 5798 . . . . . . . . . 10  |-  ( f : NN -1-1-onto-> G  ->  f : NN
--> G )
5413, 16syl6ss 3501 . . . . . . . . . 10  |-  ( ph  ->  G  C_  (  <_  i^i  ( RR  X.  RR ) ) )
55 fss 5721 . . . . . . . . . 10  |-  ( ( f : NN --> G  /\  G  C_  (  <_  i^i  ( RR  X.  RR ) ) )  -> 
f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
5653, 54, 55syl2anr 476 . . . . . . . . 9  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
57 fss 5721 . . . . . . . . . . . . . . 15  |-  ( ( f : NN --> G  /\  G  C_  ran  F )  ->  f : NN --> ran  F )
5853, 13, 57syl2anr 476 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  f : NN --> ran  F )
59 simpl 455 . . . . . . . . . . . . . 14  |-  ( ( a  e.  NN  /\  b  e.  NN )  ->  a  e.  NN )
60 ffvelrn 6005 . . . . . . . . . . . . . 14  |-  ( ( f : NN --> ran  F  /\  a  e.  NN )  ->  ( f `  a )  e.  ran  F )
6158, 59, 60syl2an 475 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( f `  a )  e.  ran  F )
62 simpr 459 . . . . . . . . . . . . . 14  |-  ( ( a  e.  NN  /\  b  e.  NN )  ->  b  e.  NN )
63 ffvelrn 6005 . . . . . . . . . . . . . 14  |-  ( ( f : NN --> ran  F  /\  b  e.  NN )  ->  ( f `  b )  e.  ran  F )
6458, 62, 63syl2an 475 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( f `  b )  e.  ran  F )
651dyaddisj 22171 . . . . . . . . . . . . 13  |-  ( ( ( f `  a
)  e.  ran  F  /\  ( f `  b
)  e.  ran  F
)  ->  ( ( [,] `  ( f `  a ) )  C_  ( [,] `  ( f `
 b ) )  \/  ( [,] `  (
f `  b )
)  C_  ( [,] `  ( f `  a
) )  \/  (
( (,) `  (
f `  a )
)  i^i  ( (,) `  ( f `  b
) ) )  =  (/) ) )
6661, 64, 65syl2anc 659 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( ( [,] `  ( f `  a ) )  C_  ( [,] `  ( f `
 b ) )  \/  ( [,] `  (
f `  b )
)  C_  ( [,] `  ( f `  a
) )  \/  (
( (,) `  (
f `  a )
)  i^i  ( (,) `  ( f `  b
) ) )  =  (/) ) )
6753adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  f : NN --> G )
68 ffvelrn 6005 . . . . . . . . . . . . . . . . 17  |-  ( ( f : NN --> G  /\  b  e.  NN )  ->  ( f `  b
)  e.  G )
6967, 62, 68syl2an 475 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( f `  b )  e.  G
)
7012, 69sseldi 3487 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( f `  b )  e.  A
)
71 ffvelrn 6005 . . . . . . . . . . . . . . . . 17  |-  ( ( f : NN --> G  /\  a  e.  NN )  ->  ( f `  a
)  e.  G )
7267, 59, 71syl2an 475 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( f `  a )  e.  G
)
73 fveq2 5848 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  ( f `  a )  ->  ( [,] `  z )  =  ( [,] `  (
f `  a )
) )
7473sseq1d 3516 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  ( f `  a )  ->  (
( [,] `  z
)  C_  ( [,] `  w )  <->  ( [,] `  ( f `  a
) )  C_  ( [,] `  w ) ) )
75 eqeq1 2458 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  ( f `  a )  ->  (
z  =  w  <->  ( f `  a )  =  w ) )
7674, 75imbi12d 318 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  ( f `  a )  ->  (
( ( [,] `  z
)  C_  ( [,] `  w )  ->  z  =  w )  <->  ( ( [,] `  ( f `  a ) )  C_  ( [,] `  w )  ->  ( f `  a )  =  w ) ) )
7776ralbidv 2893 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( f `  a )  ->  ( A. w  e.  A  ( ( [,] `  z
)  C_  ( [,] `  w )  ->  z  =  w )  <->  A. w  e.  A  ( ( [,] `  ( f `  a ) )  C_  ( [,] `  w )  ->  ( f `  a )  =  w ) ) )
7877, 2elrab2 3256 . . . . . . . . . . . . . . . . 17  |-  ( ( f `  a )  e.  G  <->  ( (
f `  a )  e.  A  /\  A. w  e.  A  ( ( [,] `  ( f `  a ) )  C_  ( [,] `  w )  ->  ( f `  a )  =  w ) ) )
7978simprbi 462 . . . . . . . . . . . . . . . 16  |-  ( ( f `  a )  e.  G  ->  A. w  e.  A  ( ( [,] `  ( f `  a ) )  C_  ( [,] `  w )  ->  ( f `  a )  =  w ) )
8072, 79syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  A. w  e.  A  ( ( [,] `  ( f `  a ) )  C_  ( [,] `  w )  ->  ( f `  a )  =  w ) )
81 fveq2 5848 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  ( f `  b )  ->  ( [,] `  w )  =  ( [,] `  (
f `  b )
) )
8281sseq2d 3517 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( f `  b )  ->  (
( [,] `  (
f `  a )
)  C_  ( [,] `  w )  <->  ( [,] `  ( f `  a
) )  C_  ( [,] `  ( f `  b ) ) ) )
83 eqeq2 2469 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( f `  b )  ->  (
( f `  a
)  =  w  <->  ( f `  a )  =  ( f `  b ) ) )
8482, 83imbi12d 318 . . . . . . . . . . . . . . . 16  |-  ( w  =  ( f `  b )  ->  (
( ( [,] `  (
f `  a )
)  C_  ( [,] `  w )  ->  (
f `  a )  =  w )  <->  ( ( [,] `  ( f `  a ) )  C_  ( [,] `  ( f `
 b ) )  ->  ( f `  a )  =  ( f `  b ) ) ) )
8584rspcv 3203 . . . . . . . . . . . . . . 15  |-  ( ( f `  b )  e.  A  ->  ( A. w  e.  A  ( ( [,] `  (
f `  a )
)  C_  ( [,] `  w )  ->  (
f `  a )  =  w )  ->  (
( [,] `  (
f `  a )
)  C_  ( [,] `  ( f `  b
) )  ->  (
f `  a )  =  ( f `  b ) ) ) )
8670, 80, 85sylc 60 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( ( [,] `  ( f `  a ) )  C_  ( [,] `  ( f `
 b ) )  ->  ( f `  a )  =  ( f `  b ) ) )
87 f1of1 5797 . . . . . . . . . . . . . . . . 17  |-  ( f : NN -1-1-onto-> G  ->  f : NN
-1-1-> G )
8887adantl 464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  f : NN -1-1-> G )
89 f1fveq 6145 . . . . . . . . . . . . . . . 16  |-  ( ( f : NN -1-1-> G  /\  ( a  e.  NN  /\  b  e.  NN ) )  ->  ( (
f `  a )  =  ( f `  b )  <->  a  =  b ) )
9088, 89sylan 469 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( (
f `  a )  =  ( f `  b )  <->  a  =  b ) )
91 orc 383 . . . . . . . . . . . . . . 15  |-  ( a  =  b  ->  (
a  =  b  \/  ( ( (,) `  (
f `  a )
)  i^i  ( (,) `  ( f `  b
) ) )  =  (/) ) )
9290, 91syl6bi 228 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( (
f `  a )  =  ( f `  b )  ->  (
a  =  b  \/  ( ( (,) `  (
f `  a )
)  i^i  ( (,) `  ( f `  b
) ) )  =  (/) ) ) )
9386, 92syld 44 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( ( [,] `  ( f `  a ) )  C_  ( [,] `  ( f `
 b ) )  ->  ( a  =  b  \/  ( ( (,) `  ( f `
 a ) )  i^i  ( (,) `  (
f `  b )
) )  =  (/) ) ) )
9412, 72sseldi 3487 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( f `  a )  e.  A
)
95 fveq2 5848 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  ( f `  b )  ->  ( [,] `  z )  =  ( [,] `  (
f `  b )
) )
9695sseq1d 3516 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  ( f `  b )  ->  (
( [,] `  z
)  C_  ( [,] `  w )  <->  ( [,] `  ( f `  b
) )  C_  ( [,] `  w ) ) )
97 eqeq1 2458 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  ( f `  b )  ->  (
z  =  w  <->  ( f `  b )  =  w ) )
9896, 97imbi12d 318 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  ( f `  b )  ->  (
( ( [,] `  z
)  C_  ( [,] `  w )  ->  z  =  w )  <->  ( ( [,] `  ( f `  b ) )  C_  ( [,] `  w )  ->  ( f `  b )  =  w ) ) )
9998ralbidv 2893 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( f `  b )  ->  ( A. w  e.  A  ( ( [,] `  z
)  C_  ( [,] `  w )  ->  z  =  w )  <->  A. w  e.  A  ( ( [,] `  ( f `  b ) )  C_  ( [,] `  w )  ->  ( f `  b )  =  w ) ) )
10099, 2elrab2 3256 . . . . . . . . . . . . . . . . 17  |-  ( ( f `  b )  e.  G  <->  ( (
f `  b )  e.  A  /\  A. w  e.  A  ( ( [,] `  ( f `  b ) )  C_  ( [,] `  w )  ->  ( f `  b )  =  w ) ) )
101100simprbi 462 . . . . . . . . . . . . . . . 16  |-  ( ( f `  b )  e.  G  ->  A. w  e.  A  ( ( [,] `  ( f `  b ) )  C_  ( [,] `  w )  ->  ( f `  b )  =  w ) )
10269, 101syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  A. w  e.  A  ( ( [,] `  ( f `  b ) )  C_  ( [,] `  w )  ->  ( f `  b )  =  w ) )
103 fveq2 5848 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  ( f `  a )  ->  ( [,] `  w )  =  ( [,] `  (
f `  a )
) )
104103sseq2d 3517 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( f `  a )  ->  (
( [,] `  (
f `  b )
)  C_  ( [,] `  w )  <->  ( [,] `  ( f `  b
) )  C_  ( [,] `  ( f `  a ) ) ) )
105 eqeq2 2469 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  ( f `  a )  ->  (
( f `  b
)  =  w  <->  ( f `  b )  =  ( f `  a ) ) )
106 eqcom 2463 . . . . . . . . . . . . . . . . . 18  |-  ( ( f `  b )  =  ( f `  a )  <->  ( f `  a )  =  ( f `  b ) )
107105, 106syl6bb 261 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( f `  a )  ->  (
( f `  b
)  =  w  <->  ( f `  a )  =  ( f `  b ) ) )
108104, 107imbi12d 318 . . . . . . . . . . . . . . . 16  |-  ( w  =  ( f `  a )  ->  (
( ( [,] `  (
f `  b )
)  C_  ( [,] `  w )  ->  (
f `  b )  =  w )  <->  ( ( [,] `  ( f `  b ) )  C_  ( [,] `  ( f `
 a ) )  ->  ( f `  a )  =  ( f `  b ) ) ) )
109108rspcv 3203 . . . . . . . . . . . . . . 15  |-  ( ( f `  a )  e.  A  ->  ( A. w  e.  A  ( ( [,] `  (
f `  b )
)  C_  ( [,] `  w )  ->  (
f `  b )  =  w )  ->  (
( [,] `  (
f `  b )
)  C_  ( [,] `  ( f `  a
) )  ->  (
f `  a )  =  ( f `  b ) ) ) )
11094, 102, 109sylc 60 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( ( [,] `  ( f `  b ) )  C_  ( [,] `  ( f `
 a ) )  ->  ( f `  a )  =  ( f `  b ) ) )
111110, 92syld 44 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( ( [,] `  ( f `  b ) )  C_  ( [,] `  ( f `
 a ) )  ->  ( a  =  b  \/  ( ( (,) `  ( f `
 a ) )  i^i  ( (,) `  (
f `  b )
) )  =  (/) ) ) )
112 olc 382 . . . . . . . . . . . . . 14  |-  ( ( ( (,) `  (
f `  a )
)  i^i  ( (,) `  ( f `  b
) ) )  =  (/)  ->  ( a  =  b  \/  ( ( (,) `  ( f `
 a ) )  i^i  ( (,) `  (
f `  b )
) )  =  (/) ) )
113112a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( (
( (,) `  (
f `  a )
)  i^i  ( (,) `  ( f `  b
) ) )  =  (/)  ->  ( a  =  b  \/  ( ( (,) `  ( f `
 a ) )  i^i  ( (,) `  (
f `  b )
) )  =  (/) ) ) )
11493, 111, 1133jaod 1290 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( (
( [,] `  (
f `  a )
)  C_  ( [,] `  ( f `  b
) )  \/  ( [,] `  ( f `  b ) )  C_  ( [,] `  ( f `
 a ) )  \/  ( ( (,) `  ( f `  a
) )  i^i  ( (,) `  ( f `  b ) ) )  =  (/) )  ->  (
a  =  b  \/  ( ( (,) `  (
f `  a )
)  i^i  ( (,) `  ( f `  b
) ) )  =  (/) ) ) )
11566, 114mpd 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f : NN -1-1-onto-> G )  /\  (
a  e.  NN  /\  b  e.  NN )
)  ->  ( a  =  b  \/  (
( (,) `  (
f `  a )
)  i^i  ( (,) `  ( f `  b
) ) )  =  (/) ) )
116115ralrimivva 2875 . . . . . . . . . 10  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  A. a  e.  NN  A. b  e.  NN  ( a  =  b  \/  ( ( (,) `  ( f `
 a ) )  i^i  ( (,) `  (
f `  b )
) )  =  (/) ) )
117 fveq2 5848 . . . . . . . . . . . 12  |-  ( a  =  b  ->  (
f `  a )  =  ( f `  b ) )
118117fveq2d 5852 . . . . . . . . . . 11  |-  ( a  =  b  ->  ( (,) `  ( f `  a ) )  =  ( (,) `  (
f `  b )
) )
119118disjor 4424 . . . . . . . . . 10  |-  (Disj  a  e.  NN  ( (,) `  (
f `  a )
)  <->  A. a  e.  NN  A. b  e.  NN  (
a  =  b  \/  ( ( (,) `  (
f `  a )
)  i^i  ( (,) `  ( f `  b
) ) )  =  (/) ) )
120116, 119sylibr 212 . . . . . . . . 9  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  -> Disj  a  e.  NN  ( (,) `  (
f `  a )
) )
121 eqid 2454 . . . . . . . . 9  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
12256, 120, 121uniiccmbl 22165 . . . . . . . 8  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  U. ran  ( [,]  o.  f )  e.  dom  vol )
12352, 122eqeltrrd 2543 . . . . . . 7  |-  ( (
ph  /\  f : NN
-1-1-onto-> G )  ->  U. ( [,] " G )  e. 
dom  vol )
124123ex 432 . . . . . 6  |-  ( ph  ->  ( f : NN -1-1-onto-> G  ->  U. ( [,] " G
)  e.  dom  vol ) )
125124exlimdv 1729 . . . . 5  |-  ( ph  ->  ( E. f  f : NN -1-1-onto-> G  ->  U. ( [,] " G )  e. 
dom  vol ) )
12644, 125syl5 32 . . . 4  |-  ( ph  ->  ( G  ~~  om  ->  U. ( [,] " G
)  e.  dom  vol ) )
127126imp 427 . . 3  |-  ( (
ph  /\  G  ~~  om )  ->  U. ( [,] " G )  e. 
dom  vol )
128 reex 9572 . . . . . . . . 9  |-  RR  e.  _V
129128, 128xpex 6577 . . . . . . . 8  |-  ( RR 
X.  RR )  e. 
_V
130129inex2 4579 . . . . . . 7  |-  (  <_  i^i  ( RR  X.  RR ) )  e.  _V
131130, 16ssexi 4582 . . . . . 6  |-  ran  F  e.  _V
132 ssdomg 7554 . . . . . 6  |-  ( ran 
F  e.  _V  ->  ( G  C_  ran  F  ->  G  ~<_  ran  F )
)
133131, 13, 132mpsyl 63 . . . . 5  |-  ( ph  ->  G  ~<_  ran  F )
134 omelon 8054 . . . . . . . 8  |-  om  e.  On
135 znnen 14030 . . . . . . . . . . . 12  |-  ZZ  ~~  NN
136135, 39entri 7562 . . . . . . . . . . 11  |-  ZZ  ~~  om
137 nn0ennn 12071 . . . . . . . . . . . 12  |-  NN0  ~~  NN
138137, 39entri 7562 . . . . . . . . . . 11  |-  NN0  ~~  om
139 xpen 7673 . . . . . . . . . . 11  |-  ( ( ZZ  ~~  om  /\  NN0  ~~  om )  ->  ( ZZ  X.  NN0 )  ~~  ( om  X.  om )
)
140136, 138, 139mp2an 670 . . . . . . . . . 10  |-  ( ZZ 
X.  NN0 )  ~~  ( om  X.  om )
141 xpomen 8384 . . . . . . . . . 10  |-  ( om 
X.  om )  ~~  om
142140, 141entri 7562 . . . . . . . . 9  |-  ( ZZ 
X.  NN0 )  ~~  om
143142ensymi 7558 . . . . . . . 8  |-  om  ~~  ( ZZ  X.  NN0 )
144 isnumi 8318 . . . . . . . 8  |-  ( ( om  e.  On  /\  om 
~~  ( ZZ  X.  NN0 ) )  ->  ( ZZ  X.  NN0 )  e. 
dom  card )
145134, 143, 144mp2an 670 . . . . . . 7  |-  ( ZZ 
X.  NN0 )  e.  dom  card
146 ffn 5713 . . . . . . . . 9  |-  ( F : ( ZZ  X.  NN0 ) --> (  <_  i^i  ( RR  X.  RR ) )  ->  F  Fn  ( ZZ  X.  NN0 ) )
14714, 146ax-mp 5 . . . . . . . 8  |-  F  Fn  ( ZZ  X.  NN0 )
148 dffn4 5783 . . . . . . . 8  |-  ( F  Fn  ( ZZ  X.  NN0 )  <->  F : ( ZZ 
X.  NN0 ) -onto-> ran  F
)
149147, 148mpbi 208 . . . . . . 7  |-  F :
( ZZ  X.  NN0 ) -onto-> ran  F
150 fodomnum 8429 . . . . . . 7  |-  ( ( ZZ  X.  NN0 )  e.  dom  card  ->  ( F : ( ZZ  X.  NN0 ) -onto-> ran  F  ->  ran  F  ~<_  ( ZZ  X.  NN0 ) ) )
151145, 149, 150mp2 9 . . . . . 6  |-  ran  F  ~<_  ( ZZ  X.  NN0 )
152 domentr 7567 . . . . . 6  |-  ( ( ran  F  ~<_  ( ZZ 
X.  NN0 )  /\  ( ZZ  X.  NN0 )  ~~  om )  ->  ran  F  ~<_  om )
153151, 142, 152mp2an 670 . . . . 5  |-  ran  F  ~<_  om
154 domtr 7561 . . . . 5  |-  ( ( G  ~<_  ran  F  /\  ran  F  ~<_  om )  ->  G  ~<_  om )
155133, 153, 154sylancl 660 . . . 4  |-  ( ph  ->  G  ~<_  om )
156 brdom2 7538 . . . 4  |-  ( G  ~<_  om  <->  ( G  ~<  om  \/  G  ~~  om ) )
157155, 156sylib 196 . . 3  |-  ( ph  ->  ( G  ~<  om  \/  G  ~~  om ) )
15838, 127, 157mpjaodan 784 . 2  |-  ( ph  ->  U. ( [,] " G
)  e.  dom  vol )
1594, 158eqeltrd 2542 1  |-  ( ph  ->  U. ( [,] " A
)  e.  dom  vol )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367    \/ w3o 970    = wceq 1398   E.wex 1617    e. wcel 1823   A.wral 2804   {crab 2808   _Vcvv 3106    i^i cin 3460    C_ wss 3461   (/)c0 3783   ~Pcpw 3999   <.cop 4022   U.cuni 4235   U_ciun 4315  Disj wdisj 4410   class class class wbr 4439   Oncon0 4867    X. cxp 4986   dom cdm 4988   ran crn 4989   "cima 4991    o. ccom 4992   Fun wfun 5564    Fn wfn 5565   -->wf 5566   -1-1->wf1 5567   -onto->wfo 5568   -1-1-onto->wf1o 5569   ` cfv 5570  (class class class)co 6270    |-> cmpt2 6272   omcom 6673   1stc1st 6771   2ndc2nd 6772    ~~ cen 7506    ~<_ cdom 7507    ~< csdm 7508   Fincfn 7509   cardccrd 8307   RRcr 9480   1c1 9482    + caddc 9484   RR*cxr 9616    <_ cle 9618    - cmin 9796    / cdiv 10202   NNcn 10531   2c2 10581   NN0cn0 10791   ZZcz 10860   (,)cioo 11532   [,]cicc 11535    seqcseq 12089   ^cexp 12148   abscabs 13149   volcvol 22041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-inf2 8049  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-fal 1404  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-disj 4411  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-se 4828  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-isom 5579  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-of 6513  df-om 6674  df-1st 6773  df-2nd 6774  df-recs 7034  df-rdg 7068  df-1o 7122  df-2o 7123  df-oadd 7126  df-omul 7127  df-er 7303  df-map 7414  df-pm 7415  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-fi 7863  df-sup 7893  df-oi 7927  df-card 8311  df-acn 8314  df-cda 8539  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-4 10592  df-n0 10792  df-z 10861  df-uz 11083  df-q 11184  df-rp 11222  df-xneg 11321  df-xadd 11322  df-xmul 11323  df-ioo 11536  df-ico 11538  df-icc 11539  df-fz 11676  df-fzo 11800  df-fl 11910  df-seq 12090  df-exp 12149  df-hash 12388  df-cj 13014  df-re 13015  df-im 13016  df-sqrt 13150  df-abs 13151  df-clim 13393  df-rlim 13394  df-sum 13591  df-rest 14912  df-topgen 14933  df-psmet 18606  df-xmet 18607  df-met 18608  df-bl 18609  df-mopn 18610  df-top 19566  df-bases 19568  df-topon 19569  df-cmp 20054  df-ovol 22042  df-vol 22043
This theorem is referenced by:  opnmbllem  22176
  Copyright terms: Public domain W3C validator