Metamath Proof Explorer

Theorem eulerpartlemelr

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 8-Aug-2018)

Ref Expression
Hypotheses eulerpartlems.r 
|- R = { f | ( `' f " NN ) e. Fin }
eulerpartlems.s 
|- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
Assertion eulerpartlemelr 
|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) )

Proof

Step Hyp Ref Expression
1 eulerpartlems.r 
 |-  R = { f | ( `' f " NN ) e. Fin }
2 eulerpartlems.s 
 |-  S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
3 inss1 
 |-  ( ( NN0 ^m NN ) i^i R ) C_ ( NN0 ^m NN )
4 3 sseli 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A e. ( NN0 ^m NN ) )
5 elmapi 
 |-  ( A e. ( NN0 ^m NN ) -> A : NN --> NN0 )
6 4 5 syl 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A : NN --> NN0 )
7 inss2 
 |-  ( ( NN0 ^m NN ) i^i R ) C_ R
8 7 sseli 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A e. R )
9 cnveq 
 |-  ( f = A -> `' f = `' A )
10 9 imaeq1d 
 |-  ( f = A -> ( `' f " NN ) = ( `' A " NN ) )
11 10 eleq1d 
 |-  ( f = A -> ( ( `' f " NN ) e. Fin <-> ( `' A " NN ) e. Fin ) )
12 11 1 elab2g 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( A e. R <-> ( `' A " NN ) e. Fin ) )
13 8 12 mpbid 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( `' A " NN ) e. Fin )
14 6 13 jca 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) )