Metamath Proof Explorer

Theorem eulerpartlem1

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 27-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses 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 ) ) } )
Assertion eulerpartlem1 
|- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )

Proof

Step Hyp Ref Expression
1 eulerpart.p 
 |-  P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
2 eulerpart.o 
 |-  O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
3 eulerpart.d 
 |-  D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
4 eulerpart.j 
 |-  J = { z e. NN | -. 2 || z }
5 eulerpart.f 
 |-  F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
6 eulerpart.h 
 |-  H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
7 eulerpart.m 
 |-  M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
8 nnex 
 |-  NN e. _V
9 4 8 rabex2 
 |-  J e. _V
10 nn0ex 
 |-  NN0 e. _V
11 eqid 
 |-  ( r e. ( ~P NN0 ^m J ) |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) = ( r e. ( ~P NN0 ^m J ) |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
12 9 10 11 6 fpwrelmapffs 
 |-  ( ( r e. ( ~P NN0 ^m J ) |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) |` H ) : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
13 ssrab2 
 |-  { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } C_ ( ( ~P NN0 i^i Fin ) ^m J )
14 10 pwex 
 |-  ~P NN0 e. _V
15 inss1 
 |-  ( ~P NN0 i^i Fin ) C_ ~P NN0
16 mapss 
 |-  ( ( ~P NN0 e. _V /\ ( ~P NN0 i^i Fin ) C_ ~P NN0 ) -> ( ( ~P NN0 i^i Fin ) ^m J ) C_ ( ~P NN0 ^m J ) )
17 14 15 16 mp2an 
 |-  ( ( ~P NN0 i^i Fin ) ^m J ) C_ ( ~P NN0 ^m J )
18 13 17 sstri 
 |-  { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } C_ ( ~P NN0 ^m J )
19 6 18 eqsstri 
 |-  H C_ ( ~P NN0 ^m J )
20 resmpt 
 |-  ( H C_ ( ~P NN0 ^m J ) -> ( ( r e. ( ~P NN0 ^m J ) |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) |` H ) = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) )
21 19 20 ax-mp 
 |-  ( ( r e. ( ~P NN0 ^m J ) |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) |` H ) = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
22 7 21 eqtr4i 
 |-  M = ( ( r e. ( ~P NN0 ^m J ) |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) |` H )
23 f1oeq1 
 |-  ( M = ( ( r e. ( ~P NN0 ^m J ) |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) |` H ) -> ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) <-> ( ( r e. ( ~P NN0 ^m J ) |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) |` H ) : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) ) )
24 22 23 ax-mp 
 |-  ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) <-> ( ( r e. ( ~P NN0 ^m J ) |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) |` H ) : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) )
25 12 24 mpbir 
 |-  M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )