Theorem reprf

Description: Members of the representation of M as the sum of S nonnegative integers from set A as functions. (Contributed by Thierry Arnoux, 5-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$$
	reprf.c	$$⊢\phi \to C\in \left(A\mathrm{repr}\left(S\right)M\right)$$
Assertion	reprf	$$⊢\phi \to C:\left(0..^S\right)⟶A$$

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		reprf.c	$$⊢\phi \to C\in \left(A\mathrm{repr}\left(S\right)M\right)$$
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	4 5	eleqtrd	$$⊢\phi \to C\in \left\{c\in \left(A^{\left(0..^S\right)}\right)|\sum _{a\in \left(0..^S\right)}c\left(a\right)=M\right\}$$
7		elrabi	$$⊢C\in \left\{c\in \left(A^{\left(0..^S\right)}\right)|\sum _{a\in \left(0..^S\right)}c\left(a\right)=M\right\}\to C\in \left(A^{\left(0..^S\right)}\right)$$
8		elmapi	$$⊢C\in \left(A^{\left(0..^S\right)}\right)\to C:\left(0..^S\right)⟶A$$
9	6 7 8	3syl	$$⊢\phi \to C:\left(0..^S\right)⟶A$$