Metamath Proof Explorer


Theorem reprfi

Description: Bounded representations are finite sets. (Contributed by Thierry Arnoux, 7-Dec-2021)

Ref Expression
Hypotheses reprval.a
|- ( ph -> A C_ NN )
reprval.m
|- ( ph -> M e. ZZ )
reprval.s
|- ( ph -> S e. NN0 )
reprfi.1
|- ( ph -> A e. Fin )
Assertion reprfi
|- ( ph -> ( A ( repr ` S ) M ) e. Fin )

Proof

Step Hyp Ref Expression
1 reprval.a
 |-  ( ph -> A C_ NN )
2 reprval.m
 |-  ( ph -> M e. ZZ )
3 reprval.s
 |-  ( ph -> S e. NN0 )
4 reprfi.1
 |-  ( ph -> A e. Fin )
5 1 2 3 reprval
 |-  ( ph -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
6 fzofi
 |-  ( 0 ..^ S ) e. Fin
7 mapfi
 |-  ( ( A e. Fin /\ ( 0 ..^ S ) e. Fin ) -> ( A ^m ( 0 ..^ S ) ) e. Fin )
8 4 6 7 sylancl
 |-  ( ph -> ( A ^m ( 0 ..^ S ) ) e. Fin )
9 rabfi
 |-  ( ( A ^m ( 0 ..^ S ) ) e. Fin -> { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } e. Fin )
10 8 9 syl
 |-  ( ph -> { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } e. Fin )
11 5 10 eqeltrd
 |-  ( ph -> ( A ( repr ` S ) M ) e. Fin )