Theorem reprfi

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

	Ref	Expression
Hypotheses	reprval.a	$$⊢\phi \to A\subseteq \mathbb{N}$$
	reprval.m	$$⊢\phi \to M\in \mathbb{Z}$$
	reprval.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
	reprfi.1	$$⊢\phi \to A\in \mathrm{Fin}$$
Assertion	reprfi	$$⊢\phi \to A\mathrm{repr}\left(S\right)M\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		reprval.a	$$⊢\phi \to A\subseteq \mathbb{N}$$
2		reprval.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		reprval.s	$$⊢\phi \to S\in {\mathbb{N}}_0$$
4		reprfi.1	$$⊢\phi \to A\in \mathrm{Fin}$$
5	1 2 3	reprval	$$⊢\phi \to A\mathrm{repr}\left(S\right)M=\left\{c\in \left(A^{\left(0..^S\right)}\right)|\sum _{a\in \left(0..^S\right)}c\left(a\right)=M\right\}$$
6		fzofi	$$⊢\left(0..^S\right)\in \mathrm{Fin}$$
7		mapfi	$$⊢\left(A\in \mathrm{Fin}\wedge \left(0..^S\right)\in \mathrm{Fin}\right)\to A^{\left(0..^S\right)}\in \mathrm{Fin}$$
8	4 6 7	sylancl	$$⊢\phi \to A^{\left(0..^S\right)}\in \mathrm{Fin}$$
9		rabfi	$$⊢A^{\left(0..^S\right)}\in \mathrm{Fin}\to \left\{c\in \left(A^{\left(0..^S\right)}\right)|\sum _{a\in \left(0..^S\right)}c\left(a\right)=M\right\}\in \mathrm{Fin}$$
10	8 9	syl	$$⊢\phi \to \left\{c\in \left(A^{\left(0..^S\right)}\right)|\sum _{a\in \left(0..^S\right)}c\left(a\right)=M\right\}\in \mathrm{Fin}$$
11	5 10	eqeltrd	$$⊢\phi \to A\mathrm{repr}\left(S\right)M\in \mathrm{Fin}$$