# 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 )`