This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )