Metamath Proof Explorer

Theorem etransclem16

Description: Every element in the range of C is a finite set. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem16.c 
|- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
etransclem16.n 
|- ( ph -> N e. NN0 )
Assertion etransclem16 
|- ( ph -> ( C ` N ) e. Fin )

Proof

Step Hyp Ref Expression
1 etransclem16.c 
 |-  C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
2 etransclem16.n 
 |-  ( ph -> N e. NN0 )
3 1 2 etransclem12 
 |-  ( ph -> ( C ` N ) = { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
4 fzfi 
 |-  ( 0 ... N ) e. Fin
5 fzfi 
 |-  ( 0 ... M ) e. Fin
6 mapfi 
 |-  ( ( ( 0 ... N ) e. Fin /\ ( 0 ... M ) e. Fin ) -> ( ( 0 ... N ) ^m ( 0 ... M ) ) e. Fin )
7 4 5 6 mp2an 
 |-  ( ( 0 ... N ) ^m ( 0 ... M ) ) e. Fin
8 ssrab2 
 |-  { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } C_ ( ( 0 ... N ) ^m ( 0 ... M ) )
9 ssfi 
 |-  ( ( ( ( 0 ... N ) ^m ( 0 ... M ) ) e. Fin /\ { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } C_ ( ( 0 ... N ) ^m ( 0 ... M ) ) ) -> { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } e. Fin )
10 7 8 9 mp2an 
 |-  { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } e. Fin
11 3 10 eqeltrdi 
 |-  ( ph -> ( C ` N ) e. Fin )