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 )