Theorem reprss

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

	Ref	Expression
Hypotheses	reprval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
	reprval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	reprval.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
	reprss.1	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
Assertion	reprss	⊢ ( 𝜑 → ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ⊆ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		reprval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2		reprval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		reprval.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4		reprss.1	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
5		nnex	⊢ ℕ ∈ V
6	5	a1i	⊢ ( 𝜑 → ℕ ∈ V )
7	6 1	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
8		mapss	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ⊆ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
9	7 4 8	syl2anc	⊢ ( 𝜑 → ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ⊆ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
10	9	sselda	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ) → 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
11	10	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) ) → 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
12	11	rabss3d	⊢ ( 𝜑 → { 𝑐 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ⊆ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
13	4 1	sstrd	⊢ ( 𝜑 → 𝐵 ⊆ ℕ )
14	13 2 3	reprval	⊢ ( 𝜑 → ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐵 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
15	1 2 3	reprval	⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
16	12 14 15	3sstr4d	⊢ ( 𝜑 → ( 𝐵 ( repr ‘ 𝑆 ) 𝑀 ) ⊆ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )