Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eulerpartgbij Structured version   Unicode version

Theorem eulerpartgbij 26777
Description: Lemma for eulerpart 26787: The  G function is a bijection. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
Hypotheses
Ref Expression
eulerpart.p  |-  P  =  { f  e.  ( NN0  ^m  NN )  |  ( ( `' f " NN )  e.  Fin  /\  sum_ k  e.  NN  (
( f `  k
)  x.  k )  =  N ) }
eulerpart.o  |-  O  =  { g  e.  P  |  A. n  e.  ( `' g " NN )  -.  2  ||  n }
eulerpart.d  |-  D  =  { g  e.  P  |  A. n  e.  NN  ( g `  n
)  <_  1 }
eulerpart.j  |-  J  =  { z  e.  NN  |  -.  2  ||  z }
eulerpart.f  |-  F  =  ( x  e.  J ,  y  e.  NN0  |->  ( ( 2 ^ y )  x.  x
) )
eulerpart.h  |-  H  =  { r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin }
eulerpart.m  |-  M  =  ( r  e.  H  |->  { <. x ,  y
>.  |  ( x  e.  J  /\  y  e.  ( r `  x
) ) } )
eulerpart.r  |-  R  =  { f  |  ( `' f " NN )  e.  Fin }
eulerpart.t  |-  T  =  { f  e.  ( NN0  ^m  NN )  |  ( `' f
" NN )  C_  J }
eulerpart.g  |-  G  =  ( o  e.  ( T  i^i  R ) 
|->  ( (𝟭 `  NN ) `  ( F " ( M `  (bits  o.  ( o  |`  J ) ) ) ) ) )
Assertion
Ref Expression
eulerpartgbij  |-  G :
( T  i^i  R
)
-1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R )
Distinct variable groups:    f, g,
k, n, o, x, y, z    o, F   
f, r, J, o, x, y    o, M, r    f, N, g, x    P, g    R, f, o    o, H, r    T, f, o
Allowed substitution hints:    D( x, y, z, f, g, k, n, o, r)    P( x, y, z, f, k, n, o, r)    R( x, y, z, g, k, n, r)    T( x, y, z, g, k, n, r)    F( x, y, z, f, g, k, n, r)    G( x, y, z, f, g, k, n, o, r)    H( x, y, z, f, g, k, n)    J( z, g, k, n)    M( x, y, z, f, g, k, n)    N( y,
z, k, n, o, r)    O( x, y, z, f, g, k, n, o, r)

Proof of Theorem eulerpartgbij
Dummy variables  a  m  b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnex 10349 . . . . 5  |-  NN  e.  _V
2 indf1ofs 26504 . . . . 5  |-  ( NN  e.  _V  ->  (
(𝟭 `  NN )  |`  Fin ) : ( ~P NN  i^i  Fin ) -1-1-onto-> {
f  e.  ( { 0 ,  1 }  ^m  NN )  |  ( `' f " { 1 } )  e.  Fin } )
31, 2ax-mp 5 . . . 4  |-  ( (𝟭 `  NN )  |`  Fin ) : ( ~P NN  i^i  Fin ) -1-1-onto-> { f  e.  ( { 0 ,  1 }  ^m  NN )  |  ( `' f
" { 1 } )  e.  Fin }
4 incom 3564 . . . . . . 7  |-  ( ( { 0 ,  1 }  ^m  NN )  i^i  { f  |  ( `' f " NN )  e.  Fin } )  =  ( { f  |  ( `' f " NN )  e.  Fin }  i^i  ( { 0 ,  1 }  ^m  NN ) )
5 eulerpart.r . . . . . . . 8  |-  R  =  { f  |  ( `' f " NN )  e.  Fin }
65ineq2i 3570 . . . . . . 7  |-  ( ( { 0 ,  1 }  ^m  NN )  i^i  R )  =  ( ( { 0 ,  1 }  ^m  NN )  i^i  { f  |  ( `' f
" NN )  e. 
Fin } )
7 dfrab2 3647 . . . . . . 7  |-  { f  e.  ( { 0 ,  1 }  ^m  NN )  |  ( `' f " NN )  e.  Fin }  =  ( { f  |  ( `' f " NN )  e.  Fin }  i^i  ( { 0 ,  1 }  ^m  NN ) )
84, 6, 73eqtr4i 2473 . . . . . 6  |-  ( ( { 0 ,  1 }  ^m  NN )  i^i  R )  =  { f  e.  ( { 0 ,  1 }  ^m  NN )  |  ( `' f
" NN )  e. 
Fin }
9 elmapi 7255 . . . . . . . . . 10  |-  ( f  e.  ( { 0 ,  1 }  ^m  NN )  ->  f : NN --> { 0 ,  1 } )
10 ffun 5582 . . . . . . . . . 10  |-  ( f : NN --> { 0 ,  1 }  ->  Fun  f )
119, 10syl 16 . . . . . . . . 9  |-  ( f  e.  ( { 0 ,  1 }  ^m  NN )  ->  Fun  f
)
12 frn 5586 . . . . . . . . . 10  |-  ( f : NN --> { 0 ,  1 }  ->  ran  f  C_  { 0 ,  1 } )
139, 12syl 16 . . . . . . . . 9  |-  ( f  e.  ( { 0 ,  1 }  ^m  NN )  ->  ran  f  C_ 
{ 0 ,  1 } )
14 fimacnvinrn2 25975 . . . . . . . . . 10  |-  ( ( Fun  f  /\  ran  f  C_  { 0 ,  1 } )  -> 
( `' f " NN )  =  ( `' f " ( NN  i^i  { 0 ,  1 } ) ) )
15 df-pr 3901 . . . . . . . . . . . . . 14  |-  { 0 ,  1 }  =  ( { 0 }  u.  { 1 } )
1615ineq2i 3570 . . . . . . . . . . . . 13  |-  ( NN 
i^i  { 0 ,  1 } )  =  ( NN  i^i  ( { 0 }  u.  {
1 } ) )
17 indi 3617 . . . . . . . . . . . . 13  |-  ( NN 
i^i  ( { 0 }  u.  { 1 } ) )  =  ( ( NN  i^i  { 0 } )  u.  ( NN  i^i  {
1 } ) )
18 0nnn 10374 . . . . . . . . . . . . . . 15  |-  -.  0  e.  NN
19 disjsn 3957 . . . . . . . . . . . . . . 15  |-  ( ( NN  i^i  { 0 } )  =  (/)  <->  -.  0  e.  NN )
2018, 19mpbir 209 . . . . . . . . . . . . . 14  |-  ( NN 
i^i  { 0 } )  =  (/)
21 1nn 10354 . . . . . . . . . . . . . . . . 17  |-  1  e.  NN
22 1ex 9402 . . . . . . . . . . . . . . . . . 18  |-  1  e.  _V
2322snss 4020 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  NN  <->  { 1 }  C_  NN )
2421, 23mpbi 208 . . . . . . . . . . . . . . . 16  |-  { 1 }  C_  NN
25 dfss 3364 . . . . . . . . . . . . . . . 16  |-  ( { 1 }  C_  NN  <->  { 1 }  =  ( { 1 }  i^i  NN ) )
2624, 25mpbi 208 . . . . . . . . . . . . . . 15  |-  { 1 }  =  ( { 1 }  i^i  NN )
27 eqcom 2445 . . . . . . . . . . . . . . . 16  |-  ( { 1 }  =  ( { 1 }  i^i  NN )  <->  ( { 1 }  i^i  NN )  =  { 1 } )
28 incom 3564 . . . . . . . . . . . . . . . . 17  |-  ( { 1 }  i^i  NN )  =  ( NN  i^i  { 1 } )
2928eqeq1i 2450 . . . . . . . . . . . . . . . 16  |-  ( ( { 1 }  i^i  NN )  =  { 1 }  <->  ( NN  i^i  { 1 } )  =  { 1 } )
3027, 29bitri 249 . . . . . . . . . . . . . . 15  |-  ( { 1 }  =  ( { 1 }  i^i  NN )  <->  ( NN  i^i  { 1 } )  =  { 1 } )
3126, 30mpbi 208 . . . . . . . . . . . . . 14  |-  ( NN 
i^i  { 1 } )  =  { 1 }
3220, 31uneq12i 3529 . . . . . . . . . . . . 13  |-  ( ( NN  i^i  { 0 } )  u.  ( NN  i^i  { 1 } ) )  =  (
(/)  u.  { 1 } )
3316, 17, 323eqtri 2467 . . . . . . . . . . . 12  |-  ( NN 
i^i  { 0 ,  1 } )  =  (
(/)  u.  { 1 } )
34 uncom 3521 . . . . . . . . . . . 12  |-  ( (/)  u. 
{ 1 } )  =  ( { 1 }  u.  (/) )
35 un0 3683 . . . . . . . . . . . 12  |-  ( { 1 }  u.  (/) )  =  { 1 }
3633, 34, 353eqtri 2467 . . . . . . . . . . 11  |-  ( NN 
i^i  { 0 ,  1 } )  =  {
1 }
3736imaeq2i 5188 . . . . . . . . . 10  |-  ( `' f " ( NN 
i^i  { 0 ,  1 } ) )  =  ( `' f " { 1 } )
3814, 37syl6eq 2491 . . . . . . . . 9  |-  ( ( Fun  f  /\  ran  f  C_  { 0 ,  1 } )  -> 
( `' f " NN )  =  ( `' f " {
1 } ) )
3911, 13, 38syl2anc 661 . . . . . . . 8  |-  ( f  e.  ( { 0 ,  1 }  ^m  NN )  ->  ( `' f " NN )  =  ( `' f
" { 1 } ) )
4039eleq1d 2509 . . . . . . 7  |-  ( f  e.  ( { 0 ,  1 }  ^m  NN )  ->  ( ( `' f " NN )  e.  Fin  <->  ( `' f " { 1 } )  e.  Fin )
)
4140rabbiia 2982 . . . . . 6  |-  { f  e.  ( { 0 ,  1 }  ^m  NN )  |  ( `' f " NN )  e.  Fin }  =  { f  e.  ( { 0 ,  1 }  ^m  NN )  |  ( `' f
" { 1 } )  e.  Fin }
428, 41eqtr2i 2464 . . . . 5  |-  { f  e.  ( { 0 ,  1 }  ^m  NN )  |  ( `' f " {
1 } )  e. 
Fin }  =  (
( { 0 ,  1 }  ^m  NN )  i^i  R )
43 f1oeq3 5655 . . . . 5  |-  ( { f  e.  ( { 0 ,  1 }  ^m  NN )  |  ( `' f " { 1 } )  e.  Fin }  =  ( ( { 0 ,  1 }  ^m  NN )  i^i  R )  ->  ( ( (𝟭 `  NN )  |`  Fin ) : ( ~P NN  i^i  Fin ) -1-1-onto-> { f  e.  ( { 0 ,  1 }  ^m  NN )  |  ( `' f
" { 1 } )  e.  Fin }  <->  ( (𝟭 `  NN )  |` 
Fin ) : ( ~P NN  i^i  Fin )
-1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R ) ) )
4442, 43ax-mp 5 . . . 4  |-  ( ( (𝟭 `  NN )  |` 
Fin ) : ( ~P NN  i^i  Fin )
-1-1-onto-> { f  e.  ( { 0 ,  1 }  ^m  NN )  |  ( `' f
" { 1 } )  e.  Fin }  <->  ( (𝟭 `  NN )  |` 
Fin ) : ( ~P NN  i^i  Fin )
-1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R ) )
453, 44mpbi 208 . . 3  |-  ( (𝟭 `  NN )  |`  Fin ) : ( ~P NN  i^i  Fin ) -1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R )
46 eulerpart.j . . . . . . 7  |-  J  =  { z  e.  NN  |  -.  2  ||  z }
47 eulerpart.f . . . . . . 7  |-  F  =  ( x  e.  J ,  y  e.  NN0  |->  ( ( 2 ^ y )  x.  x
) )
4846, 47oddpwdc 26759 . . . . . 6  |-  F :
( J  X.  NN0 )
-1-1-onto-> NN
49 f1opwfi 7636 . . . . . 6  |-  ( F : ( J  X.  NN0 ) -1-1-onto-> NN  ->  ( a  e.  ( ~P ( J  X.  NN0 )  i^i 
Fin )  |->  ( F
" a ) ) : ( ~P ( J  X.  NN0 )  i^i 
Fin ) -1-1-onto-> ( ~P NN  i^i  Fin ) )
5048, 49ax-mp 5 . . . . 5  |-  ( a  e.  ( ~P ( J  X.  NN0 )  i^i 
Fin )  |->  ( F
" a ) ) : ( ~P ( J  X.  NN0 )  i^i 
Fin ) -1-1-onto-> ( ~P NN  i^i  Fin )
51 eulerpart.p . . . . . . . 8  |-  P  =  { f  e.  ( NN0  ^m  NN )  |  ( ( `' f " NN )  e.  Fin  /\  sum_ k  e.  NN  (
( f `  k
)  x.  k )  =  N ) }
52 eulerpart.o . . . . . . . 8  |-  O  =  { g  e.  P  |  A. n  e.  ( `' g " NN )  -.  2  ||  n }
53 eulerpart.d . . . . . . . 8  |-  D  =  { g  e.  P  |  A. n  e.  NN  ( g `  n
)  <_  1 }
54 eulerpart.h . . . . . . . 8  |-  H  =  { r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin }
55 eulerpart.m . . . . . . . 8  |-  M  =  ( r  e.  H  |->  { <. x ,  y
>.  |  ( x  e.  J  /\  y  e.  ( r `  x
) ) } )
5651, 52, 53, 46, 47, 54, 55eulerpartlem1 26772 . . . . . . 7  |-  M : H
-1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin )
57 bitsf1o 13662 . . . . . . . . . . . . . 14  |-  (bits  |`  NN0 ) : NN0
-1-1-onto-> ( ~P NN0  i^i  Fin )
5857a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  (bits  |`  NN0 ) : NN0
-1-1-onto-> ( ~P NN0  i^i  Fin ) )
591rabex 4464 . . . . . . . . . . . . . . 15  |-  { z  e.  NN  |  -.  2  ||  z }  e.  _V
6046, 59eqeltri 2513 . . . . . . . . . . . . . 14  |-  J  e. 
_V
6160a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  J  e.  _V )
62 nn0ex 10606 . . . . . . . . . . . . . 14  |-  NN0  e.  _V
6362a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  NN0  e.  _V )
6462pwex 4496 . . . . . . . . . . . . . . 15  |-  ~P NN0  e.  _V
6564inex1 4454 . . . . . . . . . . . . . 14  |-  ( ~P
NN0  i^i  Fin )  e.  _V
6665a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  ( ~P NN0  i^i  Fin )  e.  _V )
67 0nn0 10615 . . . . . . . . . . . . . 14  |-  0  e.  NN0
6867a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  0  e.  NN0 )
69 fvres 5725 . . . . . . . . . . . . . . 15  |-  ( 0  e.  NN0  ->  ( (bits  |`  NN0 ) `  0
)  =  (bits ` 
0 ) )
7067, 69ax-mp 5 . . . . . . . . . . . . . 14  |-  ( (bits  |`  NN0 ) `  0
)  =  (bits ` 
0 )
71 0bits 13656 . . . . . . . . . . . . . 14  |-  (bits ` 
0 )  =  (/)
7270, 71eqtr2i 2464 . . . . . . . . . . . . 13  |-  (/)  =  ( (bits  |`  NN0 ) ` 
0 )
73 elmapi 7255 . . . . . . . . . . . . . . . . 17  |-  ( f  e.  ( NN0  ^m  J )  ->  f : J --> NN0 )
74 frnnn0supp 10654 . . . . . . . . . . . . . . . . . 18  |-  ( ( J  e.  _V  /\  f : J --> NN0 )  ->  ( f supp  0 )  =  ( `' f
" NN ) )
7560, 74mpan 670 . . . . . . . . . . . . . . . . 17  |-  ( f : J --> NN0  ->  ( f supp  0 )  =  ( `' f " NN ) )
7673, 75syl 16 . . . . . . . . . . . . . . . 16  |-  ( f  e.  ( NN0  ^m  J )  ->  (
f supp  0 )  =  ( `' f " NN ) )
7776eleq1d 2509 . . . . . . . . . . . . . . 15  |-  ( f  e.  ( NN0  ^m  J )  ->  (
( f supp  0 )  e.  Fin  <->  ( `' f " NN )  e. 
Fin ) )
7877rabbiia 2982 . . . . . . . . . . . . . 14  |-  { f  e.  ( NN0  ^m  J )  |  ( f supp  0 )  e. 
Fin }  =  {
f  e.  ( NN0 
^m  J )  |  ( `' f " NN )  e.  Fin }
79 elmapfun 7257 . . . . . . . . . . . . . . . 16  |-  ( f  e.  ( NN0  ^m  J )  ->  Fun  f )
80 vex 2996 . . . . . . . . . . . . . . . . 17  |-  f  e. 
_V
81 funisfsupp 7646 . . . . . . . . . . . . . . . . 17  |-  ( ( Fun  f  /\  f  e.  _V  /\  0  e. 
NN0 )  ->  (
f finSupp  0  <->  ( f supp  0
)  e.  Fin )
)
8280, 67, 81mp3an23 1306 . . . . . . . . . . . . . . . 16  |-  ( Fun  f  ->  ( f finSupp  0  <-> 
( f supp  0 )  e.  Fin ) )
8379, 82syl 16 . . . . . . . . . . . . . . 15  |-  ( f  e.  ( NN0  ^m  J )  ->  (
f finSupp  0  <->  ( f supp  0
)  e.  Fin )
)
8483rabbiia 2982 . . . . . . . . . . . . . 14  |-  { f  e.  ( NN0  ^m  J )  |  f finSupp 
0 }  =  {
f  e.  ( NN0 
^m  J )  |  ( f supp  0 )  e.  Fin }
85 incom 3564 . . . . . . . . . . . . . . 15  |-  ( { f  |  ( `' f " NN )  e.  Fin }  i^i  ( NN0  ^m  J ) )  =  ( ( NN0  ^m  J )  i^i  { f  |  ( `' f " NN )  e.  Fin } )
86 dfrab2 3647 . . . . . . . . . . . . . . 15  |-  { f  e.  ( NN0  ^m  J )  |  ( `' f " NN )  e.  Fin }  =  ( { f  |  ( `' f " NN )  e.  Fin }  i^i  ( NN0  ^m  J ) )
875ineq2i 3570 . . . . . . . . . . . . . . 15  |-  ( ( NN0  ^m  J )  i^i  R )  =  ( ( NN0  ^m  J )  i^i  {
f  |  ( `' f " NN )  e.  Fin } )
8885, 86, 873eqtr4ri 2474 . . . . . . . . . . . . . 14  |-  ( ( NN0  ^m  J )  i^i  R )  =  { f  e.  ( NN0  ^m  J )  |  ( `' f
" NN )  e. 
Fin }
8978, 84, 883eqtr4ri 2474 . . . . . . . . . . . . 13  |-  ( ( NN0  ^m  J )  i^i  R )  =  { f  e.  ( NN0  ^m  J )  |  f finSupp  0 }
90 elmapfun 7257 . . . . . . . . . . . . . . 15  |-  ( r  e.  ( ( ~P
NN0  i^i  Fin )  ^m  J )  ->  Fun  r )
91 vex 2996 . . . . . . . . . . . . . . . . 17  |-  r  e. 
_V
92 0ex 4443 . . . . . . . . . . . . . . . . 17  |-  (/)  e.  _V
93 funisfsupp 7646 . . . . . . . . . . . . . . . . 17  |-  ( ( Fun  r  /\  r  e.  _V  /\  (/)  e.  _V )  ->  ( r finSupp  (/)  <->  ( r supp  (/) )  e.  Fin )
)
9491, 92, 93mp3an23 1306 . . . . . . . . . . . . . . . 16  |-  ( Fun  r  ->  ( r finSupp  (/)  <->  (
r supp  (/) )  e.  Fin ) )
9594bicomd 201 . . . . . . . . . . . . . . 15  |-  ( Fun  r  ->  ( (
r supp  (/) )  e.  Fin  <->  r finSupp  (/) ) )
9690, 95syl 16 . . . . . . . . . . . . . 14  |-  ( r  e.  ( ( ~P
NN0  i^i  Fin )  ^m  J )  ->  (
( r supp  (/) )  e. 
Fin 
<->  r finSupp  (/) ) )
9796rabbiia 2982 . . . . . . . . . . . . 13  |-  { r  e.  ( ( ~P
NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e.  Fin }  =  { r  e.  ( ( ~P NN0  i^i 
Fin )  ^m  J
)  |  r finSupp  (/) }
9858, 61, 63, 66, 68, 72, 89, 97fcobijfs 26048 . . . . . . . . . . . 12  |-  ( T. 
->  ( f  e.  ( ( NN0  ^m  J
)  i^i  R )  |->  ( (bits  |`  NN0 )  o.  f ) ) : ( ( NN0  ^m  J )  i^i  R
)
-1-1-onto-> { r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin } )
99 inss1 3591 . . . . . . . . . . . . . . . . 17  |-  ( ( NN0  ^m  J )  i^i  R )  C_  ( NN0  ^m  J )
10099sseli 3373 . . . . . . . . . . . . . . . 16  |-  ( f  e.  ( ( NN0 
^m  J )  i^i 
R )  ->  f  e.  ( NN0  ^m  J
) )
101 frn 5586 . . . . . . . . . . . . . . . . 17  |-  ( f : J --> NN0  ->  ran  f  C_  NN0 )
102 cores 5362 . . . . . . . . . . . . . . . . 17  |-  ( ran  f  C_  NN0  ->  (
(bits  |`  NN0 )  o.  f )  =  (bits 
o.  f ) )
10373, 101, 1023syl 20 . . . . . . . . . . . . . . . 16  |-  ( f  e.  ( NN0  ^m  J )  ->  (
(bits  |`  NN0 )  o.  f )  =  (bits 
o.  f ) )
104100, 103syl 16 . . . . . . . . . . . . . . 15  |-  ( f  e.  ( ( NN0 
^m  J )  i^i 
R )  ->  (
(bits  |`  NN0 )  o.  f )  =  (bits 
o.  f ) )
105104mpteq2ia 4395 . . . . . . . . . . . . . 14  |-  ( f  e.  ( ( NN0 
^m  J )  i^i 
R )  |->  ( (bits  |`  NN0 )  o.  f
) )  =  ( f  e.  ( ( NN0  ^m  J )  i^i  R )  |->  (bits 
o.  f ) )
106105eqcomi 2447 . . . . . . . . . . . . 13  |-  ( f  e.  ( ( NN0 
^m  J )  i^i 
R )  |->  (bits  o.  f ) )  =  ( f  e.  ( ( NN0  ^m  J
)  i^i  R )  |->  ( (bits  |`  NN0 )  o.  f ) )
107 f1oeq1 5653 . . . . . . . . . . . . 13  |-  ( ( f  e.  ( ( NN0  ^m  J )  i^i  R )  |->  (bits 
o.  f ) )  =  ( f  e.  ( ( NN0  ^m  J )  i^i  R
)  |->  ( (bits  |`  NN0 )  o.  f ) )  -> 
( ( f  e.  ( ( NN0  ^m  J )  i^i  R
)  |->  (bits  o.  f
) ) : ( ( NN0  ^m  J
)  i^i  R ) -1-1-onto-> {
r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin }  <->  ( f  e.  ( ( NN0  ^m  J )  i^i  R
)  |->  ( (bits  |`  NN0 )  o.  f ) ) : ( ( NN0  ^m  J )  i^i  R
)
-1-1-onto-> { r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin } ) )
108106, 107mp1i 12 . . . . . . . . . . . 12  |-  ( T. 
->  ( ( f  e.  ( ( NN0  ^m  J )  i^i  R
)  |->  (bits  o.  f
) ) : ( ( NN0  ^m  J
)  i^i  R ) -1-1-onto-> {
r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin }  <->  ( f  e.  ( ( NN0  ^m  J )  i^i  R
)  |->  ( (bits  |`  NN0 )  o.  f ) ) : ( ( NN0  ^m  J )  i^i  R
)
-1-1-onto-> { r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin } ) )
10998, 108mpbird 232 . . . . . . . . . . 11  |-  ( T. 
->  ( f  e.  ( ( NN0  ^m  J
)  i^i  R )  |->  (bits  o.  f ) ) : ( ( NN0  ^m  J )  i^i  R ) -1-1-onto-> { r  e.  ( ( ~P
NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e.  Fin } )
110109trud 1378 . . . . . . . . . 10  |-  ( f  e.  ( ( NN0 
^m  J )  i^i 
R )  |->  (bits  o.  f ) ) : ( ( NN0  ^m  J )  i^i  R
)
-1-1-onto-> { r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin }
111 ssrab2 3458 . . . . . . . . . . . . . . . 16  |-  { z  e.  NN  |  -.  2  ||  z }  C_  NN
11246, 111eqsstri 3407 . . . . . . . . . . . . . . 15  |-  J  C_  NN
1131, 62, 1123pm3.2i 1166 . . . . . . . . . . . . . 14  |-  ( NN  e.  _V  /\  NN0  e.  _V  /\  J  C_  NN )
114 eulerpart.t . . . . . . . . . . . . . . . 16  |-  T  =  { f  e.  ( NN0  ^m  NN )  |  ( `' f
" NN )  C_  J }
115 cnveq 5034 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  o  ->  `' f  =  `' o
)
116 dfn2 10613 . . . . . . . . . . . . . . . . . . . 20  |-  NN  =  ( NN0  \  { 0 } )
117116a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( f  =  o  ->  NN  =  ( NN0  \  {
0 } ) )
118115, 117imaeq12d 5191 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  o  ->  ( `' f " NN )  =  ( `' o " ( NN0  \  {
0 } ) ) )
119118sseq1d 3404 . . . . . . . . . . . . . . . . 17  |-  ( f  =  o  ->  (
( `' f " NN )  C_  J  <->  ( `' o " ( NN0  \  {
0 } ) ) 
C_  J ) )
120119cbvrabv 2992 . . . . . . . . . . . . . . . 16  |-  { f  e.  ( NN0  ^m  NN )  |  ( `' f " NN )  C_  J }  =  { o  e.  ( NN0  ^m  NN )  |  ( `' o
" ( NN0  \  {
0 } ) ) 
C_  J }
121114, 120eqtri 2463 . . . . . . . . . . . . . . 15  |-  T  =  { o  e.  ( NN0  ^m  NN )  |  ( `' o
" ( NN0  \  {
0 } ) ) 
C_  J }
122 eqid 2443 . . . . . . . . . . . . . . 15  |-  ( o  e.  T  |->  ( o  |`  J ) )  =  ( o  e.  T  |->  ( o  |`  J ) )
123121, 122resf1o 26052 . . . . . . . . . . . . . 14  |-  ( ( ( NN  e.  _V  /\ 
NN0  e.  _V  /\  J  C_  NN )  /\  0  e.  NN0 )  ->  (
o  e.  T  |->  ( o  |`  J )
) : T -1-1-onto-> ( NN0 
^m  J ) )
124113, 67, 123mp2an 672 . . . . . . . . . . . . 13  |-  ( o  e.  T  |->  ( o  |`  J ) ) : T -1-1-onto-> ( NN0  ^m  J
)
125 f1of1 5661 . . . . . . . . . . . . 13  |-  ( ( o  e.  T  |->  ( o  |`  J )
) : T -1-1-onto-> ( NN0 
^m  J )  -> 
( o  e.  T  |->  ( o  |`  J ) ) : T -1-1-> ( NN0  ^m  J ) )
126124, 125ax-mp 5 . . . . . . . . . . . 12  |-  ( o  e.  T  |->  ( o  |`  J ) ) : T -1-1-> ( NN0  ^m  J )
127 inss1 3591 . . . . . . . . . . . 12  |-  ( T  i^i  R )  C_  T
128 f1ores 5676 . . . . . . . . . . . 12  |-  ( ( ( o  e.  T  |->  ( o  |`  J ) ) : T -1-1-> ( NN0  ^m  J )  /\  ( T  i^i  R )  C_  T )  ->  ( ( o  e.  T  |->  ( o  |`  J ) )  |`  ( T  i^i  R ) ) : ( T  i^i  R ) -1-1-onto-> ( ( o  e.  T  |->  ( o  |`  J )
) " ( T  i^i  R ) ) )
129126, 127, 128mp2an 672 . . . . . . . . . . 11  |-  ( ( o  e.  T  |->  ( o  |`  J )
)  |`  ( T  i^i  R ) ) : ( T  i^i  R ) -1-1-onto-> ( ( o  e.  T  |->  ( o  |`  J ) ) " ( T  i^i  R ) )
130 vex 2996 . . . . . . . . . . . . . . . . . 18  |-  o  e. 
_V
131130resex 5171 . . . . . . . . . . . . . . . . 17  |-  ( o  |`  J )  e.  _V
132131, 122fnmpti 5560 . . . . . . . . . . . . . . . 16  |-  ( o  e.  T  |->  ( o  |`  J ) )  Fn  T
133 fvelimab 5768 . . . . . . . . . . . . . . . 16  |-  ( ( ( o  e.  T  |->  ( o  |`  J ) )  Fn  T  /\  ( T  i^i  R ) 
C_  T )  -> 
( f  e.  ( ( o  e.  T  |->  ( o  |`  J ) ) " ( T  i^i  R ) )  <->  E. m  e.  ( T  i^i  R ) ( ( o  e.  T  |->  ( o  |`  J ) ) `  m )  =  f ) )
134132, 127, 133mp2an 672 . . . . . . . . . . . . . . 15  |-  ( f  e.  ( ( o  e.  T  |->  ( o  |`  J ) ) "
( T  i^i  R
) )  <->  E. m  e.  ( T  i^i  R
) ( ( o  e.  T  |->  ( o  |`  J ) ) `  m )  =  f )
135 eqid 2443 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( T  i^i  R )  |->  ( m  |`  J ) )  =  ( m  e.  ( T  i^i  R ) 
|->  ( m  |`  J ) )
136 vex 2996 . . . . . . . . . . . . . . . . . 18  |-  m  e. 
_V
137136resex 5171 . . . . . . . . . . . . . . . . 17  |-  ( m  |`  J )  e.  _V
138135, 137elrnmpti 5111 . . . . . . . . . . . . . . . 16  |-  ( f  e.  ran  ( m  e.  ( T  i^i  R )  |->  ( m  |`  J ) )  <->  E. m  e.  ( T  i^i  R
) f  =  ( m  |`  J )
)
13951, 52, 53, 46, 47, 54, 55, 5, 114eulerpartlemt 26776 . . . . . . . . . . . . . . . . 17  |-  ( ( NN0  ^m  J )  i^i  R )  =  ran  ( m  e.  ( T  i^i  R
)  |->  ( m  |`  J ) )
140139eleq2i 2507 . . . . . . . . . . . . . . . 16  |-  ( f  e.  ( ( NN0 
^m  J )  i^i 
R )  <->  f  e.  ran  ( m  e.  ( T  i^i  R ) 
|->  ( m  |`  J ) ) )
141127sseli 3373 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( T  i^i  R )  ->  m  e.  T )
142 reseq1 5125 . . . . . . . . . . . . . . . . . . . . 21  |-  ( o  =  m  ->  (
o  |`  J )  =  ( m  |`  J ) )
143142, 122, 137fvmpt 5795 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  T  ->  (
( o  e.  T  |->  ( o  |`  J ) ) `  m )  =  ( m  |`  J ) )
144143eqeq1d 2451 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  T  ->  (
( ( o  e.  T  |->  ( o  |`  J ) ) `  m )  =  f  <-> 
( m  |`  J )  =  f ) )
145141, 144syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( T  i^i  R )  ->  ( (
( o  e.  T  |->  ( o  |`  J ) ) `  m )  =  f  <->  ( m  |`  J )  =  f ) )
146 eqcom 2445 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  |`  J )  =  f  <->  f  =  ( m  |`  J )
)
147146a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( T  i^i  R )  ->  ( (
m  |`  J )  =  f  <->  f  =  ( m  |`  J )
) )
148145, 147bitrd 253 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( T  i^i  R )  ->  ( (
( o  e.  T  |->  ( o  |`  J ) ) `  m )  =  f  <->  f  =  ( m  |`  J ) ) )
149148rexbiia 2769 . . . . . . . . . . . . . . . 16  |-  ( E. m  e.  ( T  i^i  R ) ( ( o  e.  T  |->  ( o  |`  J ) ) `  m )  =  f  <->  E. m  e.  ( T  i^i  R
) f  =  ( m  |`  J )
)
150138, 140, 1493bitr4ri 278 . . . . . . . . . . . . . . 15  |-  ( E. m  e.  ( T  i^i  R ) ( ( o  e.  T  |->  ( o  |`  J ) ) `  m )  =  f  <->  f  e.  ( ( NN0  ^m  J )  i^i  R
) )
151134, 150bitri 249 . . . . . . . . . . . . . 14  |-  ( f  e.  ( ( o  e.  T  |->  ( o  |`  J ) ) "
( T  i^i  R
) )  <->  f  e.  ( ( NN0  ^m  J )  i^i  R
) )
152151eqriv 2440 . . . . . . . . . . . . 13  |-  ( ( o  e.  T  |->  ( o  |`  J )
) " ( T  i^i  R ) )  =  ( ( NN0 
^m  J )  i^i 
R )
153 f1oeq3 5655 . . . . . . . . . . . . 13  |-  ( ( ( o  e.  T  |->  ( o  |`  J ) ) " ( T  i^i  R ) )  =  ( ( NN0 
^m  J )  i^i 
R )  ->  (
( ( o  e.  T  |->  ( o  |`  J ) )  |`  ( T  i^i  R ) ) : ( T  i^i  R ) -1-1-onto-> ( ( o  e.  T  |->  ( o  |`  J )
) " ( T  i^i  R ) )  <-> 
( ( o  e.  T  |->  ( o  |`  J ) )  |`  ( T  i^i  R ) ) : ( T  i^i  R ) -1-1-onto-> ( ( NN0  ^m  J )  i^i  R ) ) )
154152, 153ax-mp 5 . . . . . . . . . . . 12  |-  ( ( ( o  e.  T  |->  ( o  |`  J ) )  |`  ( T  i^i  R ) ) : ( T  i^i  R
)
-1-1-onto-> ( ( o  e.  T  |->  ( o  |`  J ) ) "
( T  i^i  R
) )  <->  ( (
o  e.  T  |->  ( o  |`  J )
)  |`  ( T  i^i  R ) ) : ( T  i^i  R ) -1-1-onto-> ( ( NN0  ^m  J
)  i^i  R )
)
155 resmpt 5177 . . . . . . . . . . . . . 14  |-  ( ( T  i^i  R ) 
C_  T  ->  (
( o  e.  T  |->  ( o  |`  J ) )  |`  ( T  i^i  R ) )  =  ( o  e.  ( T  i^i  R ) 
|->  ( o  |`  J ) ) )
156127, 155ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( o  e.  T  |->  ( o  |`  J )
)  |`  ( T  i^i  R ) )  =  ( o  e.  ( T  i^i  R )  |->  ( o  |`  J )
)
157 f1oeq1 5653 . . . . . . . . . . . . 13  |-  ( ( ( o  e.  T  |->  ( o  |`  J ) )  |`  ( T  i^i  R ) )  =  ( o  e.  ( T  i^i  R ) 
|->  ( o  |`  J ) )  ->  ( (
( o  e.  T  |->  ( o  |`  J ) )  |`  ( T  i^i  R ) ) : ( T  i^i  R
)
-1-1-onto-> ( ( NN0  ^m  J )  i^i  R
)  <->  ( o  e.  ( T  i^i  R
)  |->  ( o  |`  J ) ) : ( T  i^i  R
)
-1-1-onto-> ( ( NN0  ^m  J )  i^i  R
) ) )
158156, 157ax-mp 5 . . . . . . . . . . . 12  |-  ( ( ( o  e.  T  |->  ( o  |`  J ) )  |`  ( T  i^i  R ) ) : ( T  i^i  R
)
-1-1-onto-> ( ( NN0  ^m  J )  i^i  R
)  <->  ( o  e.  ( T  i^i  R
)  |->  ( o  |`  J ) ) : ( T  i^i  R
)
-1-1-onto-> ( ( NN0  ^m  J )  i^i  R
) )
159154, 158bitri 249 . . . . . . . . . . 11  |-  ( ( ( o  e.  T  |->  ( o  |`  J ) )  |`  ( T  i^i  R ) ) : ( T  i^i  R
)
-1-1-onto-> ( ( o  e.  T  |->  ( o  |`  J ) ) "
( T  i^i  R
) )  <->  ( o  e.  ( T  i^i  R
)  |->  ( o  |`  J ) ) : ( T  i^i  R
)
-1-1-onto-> ( ( NN0  ^m  J )  i^i  R
) )
160129, 159mpbi 208 . . . . . . . . . 10  |-  ( o  e.  ( T  i^i  R )  |->  ( o  |`  J ) ) : ( T  i^i  R
)
-1-1-onto-> ( ( NN0  ^m  J )  i^i  R
)
161 f1oco 5684 . . . . . . . . . 10  |-  ( ( ( f  e.  ( ( NN0  ^m  J
)  i^i  R )  |->  (bits  o.  f ) ) : ( ( NN0  ^m  J )  i^i  R ) -1-1-onto-> { r  e.  ( ( ~P
NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e.  Fin }  /\  ( o  e.  ( T  i^i  R
)  |->  ( o  |`  J ) ) : ( T  i^i  R
)
-1-1-onto-> ( ( NN0  ^m  J )  i^i  R
) )  ->  (
( f  e.  ( ( NN0  ^m  J
)  i^i  R )  |->  (bits  o.  f ) )  o.  ( o  e.  ( T  i^i  R )  |->  ( o  |`  J ) ) ) : ( T  i^i  R ) -1-1-onto-> { r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin } )
162110, 160, 161mp2an 672 . . . . . . . . 9  |-  ( ( f  e.  ( ( NN0  ^m  J )  i^i  R )  |->  (bits 
o.  f ) )  o.  ( o  e.  ( T  i^i  R
)  |->  ( o  |`  J ) ) ) : ( T  i^i  R ) -1-1-onto-> { r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin }
163 f1of 5662 . . . . . . . . . . . . . . 15  |-  ( ( o  e.  ( T  i^i  R )  |->  ( o  |`  J )
) : ( T  i^i  R ) -1-1-onto-> ( ( NN0  ^m  J )  i^i  R )  -> 
( o  e.  ( T  i^i  R ) 
|->  ( o  |`  J ) ) : ( T  i^i  R ) --> ( ( NN0  ^m  J
)  i^i  R )
)
164 eqid 2443 . . . . . . . . . . . . . . . . 17  |-  ( o  e.  ( T  i^i  R )  |->  ( o  |`  J ) )  =  ( o  e.  ( T  i^i  R ) 
|->  ( o  |`  J ) )
165164fmpt 5885 . . . . . . . . . . . . . . . 16  |-  ( A. o  e.  ( T  i^i  R ) ( o  |`  J )  e.  ( ( NN0  ^m  J
)  i^i  R )  <->  ( o  e.  ( T  i^i  R )  |->  ( o  |`  J )
) : ( T  i^i  R ) --> ( ( NN0  ^m  J
)  i^i  R )
)
166165biimpri 206 . . . . . . . . . . . . . . 15  |-  ( ( o  e.  ( T  i^i  R )  |->  ( o  |`  J )
) : ( T  i^i  R ) --> ( ( NN0  ^m  J
)  i^i  R )  ->  A. o  e.  ( T  i^i  R ) ( o  |`  J )  e.  ( ( NN0 
^m  J )  i^i 
R ) )
167160, 163, 166mp2b 10 . . . . . . . . . . . . . 14  |-  A. o  e.  ( T  i^i  R
) ( o  |`  J )  e.  ( ( NN0  ^m  J
)  i^i  R )
168167a1i 11 . . . . . . . . . . . . 13  |-  ( T. 
->  A. o  e.  ( T  i^i  R ) ( o  |`  J )  e.  ( ( NN0 
^m  J )  i^i 
R ) )
169168r19.21bi 2835 . . . . . . . . . . . 12  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  (
o  |`  J )  e.  ( ( NN0  ^m  J )  i^i  R
) )
170 eqidd 2444 . . . . . . . . . . . 12  |-  ( T. 
->  ( o  e.  ( T  i^i  R ) 
|->  ( o  |`  J ) )  =  ( o  e.  ( T  i^i  R )  |->  ( o  |`  J ) ) )
171 eqidd 2444 . . . . . . . . . . . 12  |-  ( T. 
->  ( f  e.  ( ( NN0  ^m  J
)  i^i  R )  |->  (bits  o.  f ) )  =  ( f  e.  ( ( NN0 
^m  J )  i^i 
R )  |->  (bits  o.  f ) ) )
172 coeq2 5019 . . . . . . . . . . . 12  |-  ( f  =  ( o  |`  J )  ->  (bits  o.  f )  =  (bits 
o.  ( o  |`  J ) ) )
173169, 170, 171, 172fmptco 5897 . . . . . . . . . . 11  |-  ( T. 
->  ( ( f  e.  ( ( NN0  ^m  J )  i^i  R
)  |->  (bits  o.  f
) )  o.  (
o  e.  ( T  i^i  R )  |->  ( o  |`  J )
) )  =  ( o  e.  ( T  i^i  R )  |->  (bits 
o.  ( o  |`  J ) ) ) )
174173eqcomd 2448 . . . . . . . . . 10  |-  ( T. 
->  ( o  e.  ( T  i^i  R ) 
|->  (bits  o.  ( o  |`  J ) ) )  =  ( ( f  e.  ( ( NN0 
^m  J )  i^i 
R )  |->  (bits  o.  f ) )  o.  ( o  e.  ( T  i^i  R ) 
|->  ( o  |`  J ) ) ) )
175 eqidd 2444 . . . . . . . . . 10  |-  ( T. 
->  ( T  i^i  R
)  =  ( T  i^i  R ) )
17654a1i 11 . . . . . . . . . 10  |-  ( T. 
->  H  =  {
r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin } )
177174, 175, 176f1oeq123d 5659 . . . . . . . . 9  |-  ( T. 
->  ( ( o  e.  ( T  i^i  R
)  |->  (bits  o.  (
o  |`  J ) ) ) : ( T  i^i  R ) -1-1-onto-> H  <->  ( (
f  e.  ( ( NN0  ^m  J )  i^i  R )  |->  (bits 
o.  f ) )  o.  ( o  e.  ( T  i^i  R
)  |->  ( o  |`  J ) ) ) : ( T  i^i  R ) -1-1-onto-> { r  e.  ( ( ~P NN0  i^i  Fin )  ^m  J )  |  ( r supp  (/) )  e. 
Fin } ) )
178162, 177mpbiri 233 . . . . . . . 8  |-  ( T. 
->  ( o  e.  ( T  i^i  R ) 
|->  (bits  o.  ( o  |`  J ) ) ) : ( T  i^i  R ) -1-1-onto-> H )
179178trud 1378 . . . . . . 7  |-  ( o  e.  ( T  i^i  R )  |->  (bits  o.  (
o  |`  J ) ) ) : ( T  i^i  R ) -1-1-onto-> H
180 f1oco 5684 . . . . . . 7  |-  ( ( M : H -1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin )  /\  ( o  e.  ( T  i^i  R ) 
|->  (bits  o.  ( o  |`  J ) ) ) : ( T  i^i  R ) -1-1-onto-> H )  ->  ( M  o.  ( o  e.  ( T  i^i  R
)  |->  (bits  o.  (
o  |`  J ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin )
)
18156, 179, 180mp2an 672 . . . . . 6  |-  ( M  o.  ( o  e.  ( T  i^i  R
)  |->  (bits  o.  (
o  |`  J ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin )
182 eqidd 2444 . . . . . . . . . . 11  |-  ( T. 
->  ( o  e.  ( T  i^i  R ) 
|->  (bits  o.  ( o  |`  J ) ) )  =  ( o  e.  ( T  i^i  R
)  |->  (bits  o.  (
o  |`  J ) ) ) )
183 bitsf 13644 . . . . . . . . . . . . . 14  |- bits : ZZ --> ~P NN0
184 zex 10676 . . . . . . . . . . . . . 14  |-  ZZ  e.  _V
185 fex 5971 . . . . . . . . . . . . . 14  |-  ( (bits
: ZZ --> ~P NN0  /\  ZZ  e.  _V )  -> bits  e.  _V )
186183, 184, 185mp2an 672 . . . . . . . . . . . . 13  |- bits  e.  _V
187186, 131coex 6550 . . . . . . . . . . . 12  |-  (bits  o.  ( o  |`  J ) )  e.  _V
188187a1i 11 . . . . . . . . . . 11  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  (bits  o.  ( o  |`  J ) )  e.  _V )
189182, 188fvmpt2d 5804 . . . . . . . . . 10  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  (
( o  e.  ( T  i^i  R ) 
|->  (bits  o.  ( o  |`  J ) ) ) `
 o )  =  (bits  o.  ( o  |`  J ) ) )
190 f1of 5662 . . . . . . . . . . . 12  |-  ( ( o  e.  ( T  i^i  R )  |->  (bits 
o.  ( o  |`  J ) ) ) : ( T  i^i  R ) -1-1-onto-> H  ->  ( o  e.  ( T  i^i  R
)  |->  (bits  o.  (
o  |`  J ) ) ) : ( T  i^i  R ) --> H )
191179, 190mp1i 12 . . . . . . . . . . 11  |-  ( T. 
->  ( o  e.  ( T  i^i  R ) 
|->  (bits  o.  ( o  |`  J ) ) ) : ( T  i^i  R ) --> H )
192191ffvelrnda 5864 . . . . . . . . . 10  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  (
( o  e.  ( T  i^i  R ) 
|->  (bits  o.  ( o  |`  J ) ) ) `
 o )  e.  H )
193189, 192eqeltrrd 2518 . . . . . . . . 9  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  (bits  o.  ( o  |`  J ) )  e.  H )
194 f1ofn 5663 . . . . . . . . . . . 12  |-  ( M : H -1-1-onto-> ( ~P ( J  X.  NN0 )  i^i 
Fin )  ->  M  Fn  H )
19556, 194ax-mp 5 . . . . . . . . . . 11  |-  M  Fn  H
196 dffn5 5758 . . . . . . . . . . 11  |-  ( M  Fn  H  <->  M  =  ( r  e.  H  |->  ( M `  r
) ) )
197195, 196mpbi 208 . . . . . . . . . 10  |-  M  =  ( r  e.  H  |->  ( M `  r
) )
198197a1i 11 . . . . . . . . 9  |-  ( T. 
->  M  =  (
r  e.  H  |->  ( M `  r ) ) )
199 fveq2 5712 . . . . . . . . 9  |-  ( r  =  (bits  o.  (
o  |`  J ) )  ->  ( M `  r )  =  ( M `  (bits  o.  ( o  |`  J ) ) ) )
200193, 182, 198, 199fmptco 5897 . . . . . . . 8  |-  ( T. 
->  ( M  o.  (
o  e.  ( T  i^i  R )  |->  (bits 
o.  ( o  |`  J ) ) ) )  =  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) )
201200trud 1378 . . . . . . 7  |-  ( M  o.  ( o  e.  ( T  i^i  R
)  |->  (bits  o.  (
o  |`  J ) ) ) )  =  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) )
202 f1oeq1 5653 . . . . . . 7  |-  ( ( M  o.  ( o  e.  ( T  i^i  R )  |->  (bits  o.  (
o  |`  J ) ) ) )  =  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) )  -> 
( ( M  o.  ( o  e.  ( T  i^i  R ) 
|->  (bits  o.  ( o  |`  J ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin )  <->  ( o  e.  ( T  i^i  R
)  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin ) ) )
203201, 202ax-mp 5 . . . . . 6  |-  ( ( M  o.  ( o  e.  ( T  i^i  R )  |->  (bits  o.  (
o  |`  J ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin )  <->  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) : ( T  i^i  R
)
-1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin )
)
204181, 203mpbi 208 . . . . 5  |-  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin )
205 f1oco 5684 . . . . 5  |-  ( ( ( a  e.  ( ~P ( J  X.  NN0 )  i^i  Fin )  |->  ( F " a
) ) : ( ~P ( J  X.  NN0 )  i^i  Fin ) -1-1-onto-> ( ~P NN  i^i  Fin )  /\  ( o  e.  ( T  i^i  R ) 
|->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) : ( T  i^i  R
)
-1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin )
)  ->  ( (
a  e.  ( ~P ( J  X.  NN0 )  i^i  Fin )  |->  ( F " a ) )  o.  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P NN  i^i  Fin ) )
20650, 204, 205mp2an 672 . . . 4  |-  ( ( a  e.  ( ~P ( J  X.  NN0 )  i^i  Fin )  |->  ( F " a ) )  o.  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P NN  i^i  Fin )
207 simpr 461 . . . . . . . . 9  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  o  e.  ( T  i^i  R
) )
208 fvex 5722 . . . . . . . . . 10  |-  ( M `
 (bits  o.  (
o  |`  J ) ) )  e.  _V
209208a1i 11 . . . . . . . . 9  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  ( M `  (bits  o.  (
o  |`  J ) ) )  e.  _V )
210 eqid 2443 . . . . . . . . . 10  |-  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) )  =  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) )
211210fvmpt2 5802 . . . . . . . . 9  |-  ( ( o  e.  ( T  i^i  R )  /\  ( M `  (bits  o.  ( o  |`  J ) ) )  e.  _V )  ->  ( ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) `  o )  =  ( M `  (bits  o.  ( o  |`  J ) ) ) )
212207, 209, 211syl2anc 661 . . . . . . . 8  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  (
( o  e.  ( T  i^i  R ) 
|->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) `  o )  =  ( M `  (bits  o.  ( o  |`  J ) ) ) )
213 f1of 5662 . . . . . . . . . 10  |-  ( ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) : ( T  i^i  R
)
-1-1-onto-> ( ~P ( J  X.  NN0 )  i^i  Fin )  ->  ( o  e.  ( T  i^i  R ) 
|->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) : ( T  i^i  R
) --> ( ~P ( J  X.  NN0 )  i^i 
Fin ) )
214204, 213mp1i 12 . . . . . . . . 9  |-  ( T. 
->  ( o  e.  ( T  i^i  R ) 
|->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) : ( T  i^i  R
) --> ( ~P ( J  X.  NN0 )  i^i 
Fin ) )
215214ffvelrnda 5864 . . . . . . . 8  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  (
( o  e.  ( T  i^i  R ) 
|->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) `  o )  e.  ( ~P ( J  X.  NN0 )  i^i  Fin )
)
216212, 215eqeltrrd 2518 . . . . . . 7  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  ( M `  (bits  o.  (
o  |`  J ) ) )  e.  ( ~P ( J  X.  NN0 )  i^i  Fin ) )
217 eqidd 2444 . . . . . . 7  |-  ( T. 
->  ( o  e.  ( T  i^i  R ) 
|->  ( M `  (bits  o.  ( o  |`  J ) ) ) )  =  ( o  e.  ( T  i^i  R ) 
|->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) )
218 eqidd 2444 . . . . . . 7  |-  ( T. 
->  ( a  e.  ( ~P ( J  X.  NN0 )  i^i  Fin )  |->  ( F " a
) )  =  ( a  e.  ( ~P ( J  X.  NN0 )  i^i  Fin )  |->  ( F " a ) ) )
219 imaeq2 5186 . . . . . . 7  |-  ( a  =  ( M `  (bits  o.  ( o  |`  J ) ) )  ->  ( F "
a )  =  ( F " ( M `
 (bits  o.  (
o  |`  J ) ) ) ) )
220216, 217, 218, 219fmptco 5897 . . . . . 6  |-  ( T. 
->  ( ( a  e.  ( ~P ( J  X.  NN0 )  i^i 
Fin )  |->  ( F
" a ) )  o.  ( o  e.  ( T  i^i  R
)  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) )  =  ( o  e.  ( T  i^i  R )  |->  ( F " ( M `
 (bits  o.  (
o  |`  J ) ) ) ) ) )
221220trud 1378 . . . . 5  |-  ( ( a  e.  ( ~P ( J  X.  NN0 )  i^i  Fin )  |->  ( F " a ) )  o.  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) )  =  ( o  e.  ( T  i^i  R )  |->  ( F " ( M `
 (bits  o.  (
o  |`  J ) ) ) ) )
222 f1oeq1 5653 . . . . 5  |-  ( ( ( a  e.  ( ~P ( J  X.  NN0 )  i^i  Fin )  |->  ( F " a
) )  o.  (
o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) )  =  ( o  e.  ( T  i^i  R
)  |->  ( F "
( M `  (bits  o.  ( o  |`  J ) ) ) ) )  ->  ( ( ( a  e.  ( ~P ( J  X.  NN0 )  i^i  Fin )  |->  ( F " a ) )  o.  ( o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P NN  i^i  Fin ) 
<->  ( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) : ( T  i^i  R
)
-1-1-onto-> ( ~P NN  i^i  Fin ) ) )
223221, 222ax-mp 5 . . . 4  |-  ( ( ( a  e.  ( ~P ( J  X.  NN0 )  i^i  Fin )  |->  ( F " a
) )  o.  (
o  e.  ( T  i^i  R )  |->  ( M `  (bits  o.  ( o  |`  J ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P NN  i^i  Fin )  <->  ( o  e.  ( T  i^i  R
)  |->  ( F "
( M `  (bits  o.  ( o  |`  J ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P NN  i^i  Fin ) )
224206, 223mpbi 208 . . 3  |-  ( o  e.  ( T  i^i  R )  |->  ( F "
( M `  (bits  o.  ( o  |`  J ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P NN  i^i  Fin )
225 f1oco 5684 . . 3  |-  ( ( ( (𝟭 `  NN )  |`  Fin ) : ( ~P NN  i^i  Fin ) -1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R )  /\  ( o  e.  ( T  i^i  R
)  |->  ( F "
( M `  (bits  o.  ( o  |`  J ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ~P NN  i^i  Fin ) )  ->  (
( (𝟭 `  NN )  |` 
Fin )  o.  (
o  e.  ( T  i^i  R )  |->  ( F " ( M `
 (bits  o.  (
o  |`  J ) ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R ) )
22645, 224, 225mp2an 672 . 2  |-  ( ( (𝟭 `  NN )  |` 
Fin )  o.  (
o  e.  ( T  i^i  R )  |->  ( F " ( M `
 (bits  o.  (
o  |`  J ) ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R )
227 eulerpart.g . . . 4  |-  G  =  ( o  e.  ( T  i^i  R ) 
|->  ( (𝟭 `  NN ) `  ( F " ( M `  (bits  o.  ( o  |`  J ) ) ) ) ) )
22847mpt2exg 6669 . . . . . . . . . . 11  |-  ( ( J  e.  _V  /\  NN0 
e.  _V )  ->  F  e.  _V )
22960, 62, 228mp2an 672 . . . . . . . . . 10  |-  F  e. 
_V
230 imaexg 6536 . . . . . . . . . 10  |-  ( F  e.  _V  ->  ( F " ( M `  (bits  o.  ( o  |`  J ) ) ) )  e.  _V )
231229, 230ax-mp 5 . . . . . . . . 9  |-  ( F
" ( M `  (bits  o.  ( o  |`  J ) ) ) )  e.  _V
232231a1i 11 . . . . . . . 8  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  ( F " ( M `  (bits  o.  ( o  |`  J ) ) ) )  e.  _V )
233 eqid 2443 . . . . . . . . 9  |-  ( o  e.  ( T  i^i  R )  |->  ( F "
( M `  (bits  o.  ( o  |`  J ) ) ) ) )  =  ( o  e.  ( T  i^i  R
)  |->  ( F "
( M `  (bits  o.  ( o  |`  J ) ) ) ) )
234233fvmpt2 5802 . . . . . . . 8  |-  ( ( o  e.  ( T  i^i  R )  /\  ( F " ( M `
 (bits  o.  (
o  |`  J ) ) ) )  e.  _V )  ->  ( ( o  e.  ( T  i^i  R )  |->  ( F "
( M `  (bits  o.  ( o  |`  J ) ) ) ) ) `
 o )  =  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) )
235207, 232, 234syl2anc 661 . . . . . . 7  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  (
( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) `  o )  =  ( F " ( M `
 (bits  o.  (
o  |`  J ) ) ) ) )
236 f1of 5662 . . . . . . . . 9  |-  ( ( o  e.  ( T  i^i  R )  |->  ( F " ( M `
 (bits  o.  (
o  |`  J ) ) ) ) ) : ( T  i^i  R
)
-1-1-onto-> ( ~P NN  i^i  Fin )  ->  ( o  e.  ( T  i^i  R
)  |->  ( F "
( M `  (bits  o.  ( o  |`  J ) ) ) ) ) : ( T  i^i  R ) --> ( ~P NN  i^i  Fin ) )
237224, 236mp1i 12 . . . . . . . 8  |-  ( T. 
->  ( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) : ( T  i^i  R
) --> ( ~P NN  i^i  Fin ) )
238237ffvelrnda 5864 . . . . . . 7  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  (
( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) `  o )  e.  ( ~P NN  i^i  Fin ) )
239235, 238eqeltrrd 2518 . . . . . 6  |-  ( ( T.  /\  o  e.  ( T  i^i  R
) )  ->  ( F " ( M `  (bits  o.  ( o  |`  J ) ) ) )  e.  ( ~P NN  i^i  Fin )
)
240 eqidd 2444 . . . . . 6  |-  ( T. 
->  ( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) )  =  ( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) )
241 indf1o 26502 . . . . . . . . . . 11  |-  ( NN  e.  _V  ->  (𝟭 `  NN ) : ~P NN
-1-1-onto-> ( { 0 ,  1 }  ^m  NN ) )
242 f1ofn 5663 . . . . . . . . . . 11  |-  ( (𝟭 `  NN ) : ~P NN
-1-1-onto-> ( { 0 ,  1 }  ^m  NN )  ->  (𝟭 `  NN )  Fn  ~P NN )
2431, 241, 242mp2b 10 . . . . . . . . . 10  |-  (𝟭 `  NN )  Fn  ~P NN
244 dffn5 5758 . . . . . . . . . 10  |-  ( (𝟭 `  NN )  Fn  ~P NN 
<->  (𝟭 `  NN )  =  ( b  e. 
~P NN  |->  ( (𝟭 `  NN ) `  b
) ) )
245243, 244mpbi 208 . . . . . . . . 9  |-  (𝟭 `  NN )  =  ( b  e.  ~P NN  |->  ( (𝟭 `  NN ) `  b
) )
246245reseq1i 5127 . . . . . . . 8  |-  ( (𝟭 `  NN )  |`  Fin )  =  ( ( b  e.  ~P NN  |->  ( (𝟭 `  NN ) `  b ) )  |`  Fin )
247 resmpt3 5178 . . . . . . . 8  |-  ( ( b  e.  ~P NN  |->  ( (𝟭 `  NN ) `  b ) )  |`  Fin )  =  (
b  e.  ( ~P NN  i^i  Fin )  |->  ( (𝟭 `  NN ) `  b )
)
248246, 247eqtri 2463 . . . . . . 7  |-  ( (𝟭 `  NN )  |`  Fin )  =  ( b  e.  ( ~P NN  i^i  Fin )  |->  ( (𝟭 `  NN ) `  b )
)
249248a1i 11 . . . . . 6  |-  ( T. 
->  ( (𝟭 `  NN )  |`  Fin )  =  ( b  e.  ( ~P NN  i^i  Fin )  |->  ( (𝟭 `  NN ) `  b )
) )
250 fveq2 5712 . . . . . 6  |-  ( b  =  ( F "
( M `  (bits  o.  ( o  |`  J ) ) ) )  -> 
( (𝟭 `  NN ) `  b )  =  ( (𝟭 `  NN ) `  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) )
251239, 240, 249, 250fmptco 5897 . . . . 5  |-  ( T. 
->  ( ( (𝟭 `  NN )  |`  Fin )  o.  ( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) )  =  ( o  e.  ( T  i^i  R
)  |->  ( (𝟭 `  NN ) `  ( F " ( M `  (bits  o.  ( o  |`  J ) ) ) ) ) ) )
252251trud 1378 . . . 4  |-  ( ( (𝟭 `  NN )  |` 
Fin )  o.  (
o  e.  ( T  i^i  R )  |->  ( F " ( M `
 (bits  o.  (
o  |`  J ) ) ) ) ) )  =  ( o  e.  ( T  i^i  R
)  |->  ( (𝟭 `  NN ) `  ( F " ( M `  (bits  o.  ( o  |`  J ) ) ) ) ) )
253227, 252eqtr4i 2466 . . 3  |-  G  =  ( ( (𝟭 `  NN )  |`  Fin )  o.  ( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) )
254 f1oeq1 5653 . . 3  |-  ( G  =  ( ( (𝟭 `  NN )  |`  Fin )  o.  ( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) )  ->  ( G :
( T  i^i  R
)
-1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R )  <-> 
( ( (𝟭 `  NN )  |`  Fin )  o.  ( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R ) ) )
255253, 254ax-mp 5 . 2  |-  ( G : ( T  i^i  R ) -1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R )  <-> 
( ( (𝟭 `  NN )  |`  Fin )  o.  ( o  e.  ( T  i^i  R ) 
|->  ( F " ( M `  (bits  o.  (
o  |`  J ) ) ) ) ) ) : ( T  i^i  R ) -1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R ) )
256226, 255mpbir 209 1  |-  G :
( T  i^i  R
)
-1-1-onto-> ( ( { 0 ,  1 }  ^m  NN )  i^i  R )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369   T. wtru 1370    e. wcel 1756   {cab 2429   A.wral 2736   E.wrex 2737   {crab 2740   _Vcvv 2993    \ cdif 3346    u. cun 3347    i^i cin 3348    C_ wss 3349   (/)c0 3658   ~Pcpw 3881   {csn 3898   {cpr 3900   class class class wbr 4313   {copab 4370    e. cmpt 4371    X. cxp 4859   `'ccnv 4860   ran crn 4862    |` cres 4863   "cima 4864    o. ccom 4865   Fun wfun 5433    Fn wfn 5434   -->wf 5435   -1-1->wf1 5436   -1-1-onto->wf1o 5438   ` cfv 5439  (class class class)co 6112    e. cmpt2 6114   supp csupp 6711    ^m cmap 7235   Fincfn 7331   finSupp cfsupp 7641   0cc0 9303   1c1 9304    x. cmul 9308    <_ cle 9440   NNcn 10343   2c2 10392   NN0cn0 10600   ZZcz 10667   ^cexp 11886   sum_csu 13184    || cdivides 13556  bitscbits 13636  𝟭cind 26489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-inf2 7868  ax-ac2 8653  ax-cnex 9359  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-mulcom 9367  ax-addass 9368  ax-mulass 9369  ax-distr 9370  ax-i2m1 9371  ax-1ne0 9372  ax-1rid 9373  ax-rnegex 9374  ax-rrecex 9375  ax-cnre 9376  ax-pre-lttri 9377  ax-pre-lttrn 9378  ax-pre-ltadd 9379  ax-pre-mulgt0 9380  ax-pre-sup 9381
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-disj 4284  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-se 4701  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-isom 5448  df-riota 6073  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-1st 6598  df-2nd 6599  df-supp 6712  df-recs 6853  df-rdg 6887  df-1o 6941  df-2o 6942  df-oadd 6945  df-er 7122  df-map 7237  df-pm 7238  df-en 7332  df-dom 7333  df-sdom 7334  df-fin 7335  df-fsupp 7642  df-sup 7712  df-oi 7745  df-card 8130  df-acn 8133  df-ac 8307  df-cda 8358  df-pnf 9441  df-mnf 9442  df-xr 9443  df-ltxr 9444  df-le 9445  df-sub 9618  df-neg 9619  df-div 10015  df-nn 10344  df-2 10401  df-3 10402  df-n0 10601  df-z 10668  df-uz 10883  df-rp 11013  df-fz 11459  df-fzo 11570  df-fl 11663  df-mod 11730  df-seq 11828  df-exp 11887  df-hash 12125  df-cj 12609  df-re 12610  df-im 12611  df-sqr 12745  df-abs 12746  df-clim 12987  df-sum 13185  df-dvds 13557  df-bits 13639  df-ind 26490
This theorem is referenced by:  eulerpartlemgf  26784  eulerpartlemgs2  26785  eulerpartlemn  26786
  Copyright terms: Public domain W3C validator