reprss

Description: Representations with terms in a subset. (Contributed by Thierry Arnoux, 11-Dec-2021)

	Ref	Expression
Hypotheses	reprval.a	$⊢ φ \to A \subseteq ℕ$
	reprval.m	$⊢ φ \to M \in ℤ$
	reprval.s	$⊢ φ \to S \in ℕ_{0}$
	reprss.1	$⊢ φ \to B \subseteq A$
Assertion	reprss	$⊢ φ \to B repr (S) M \subseteq A repr (S) M$

Step	Hyp	Ref	Expression
1		reprval.a	$⊢ φ \to A \subseteq ℕ$
2		reprval.m	$⊢ φ \to M \in ℤ$
3		reprval.s	$⊢ φ \to S \in ℕ_{0}$
4		reprss.1	$⊢ φ \to B \subseteq A$
5		nnex	$⊢ ℕ \in V$
6	5	a1i	$⊢ φ \to ℕ \in V$
7	6 1	ssexd	$⊢ φ \to A \in V$
8		mapss	$⊢ (A \in V \land B \subseteq A) \to B^{(0 ..^S)} \subseteq A^{(0 ..^S)}$
9	7 4 8	syl2anc	$⊢ φ \to B^{(0 ..^S)} \subseteq A^{(0 ..^S)}$
10	9	sselda	$⊢ (φ \land c \in (B^{(0 ..^S)})) \to c \in (A^{(0 ..^S)})$
11	10	adantrr	$⊢ (φ \land (c \in (B^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} c (a) = M)) \to c \in (A^{(0 ..^S)})$
12	11	rabss3d	$⊢ φ \to \{c \in (B^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\} \subseteq \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
13	4 1	sstrd	$⊢ φ \to B \subseteq ℕ$
14	13 2 3	reprval	$⊢ φ \to B repr (S) M = \{c \in (B^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
15	1 2 3	reprval	$⊢ φ \to A repr (S) M = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
16	12 14 15	3sstr4d	$⊢ φ \to B repr (S) M \subseteq A repr (S) M$

Metamath Proof Explorer