Metamath Proof Explorer

Theorem reprss

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

Ref Expression
Hypotheses reprval.a ⊢ φ → A ⊆ ℕ
reprval.m ⊢ φ → M ∈ ℤ
reprval.s ⊢ φ → S ∈ ℕ 0
reprss.1 ⊢ φ → B ⊆ A
Assertion reprss ⊢ φ → B repr ⁡ S M ⊆ A repr ⁡ S M

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ φ → A ⊆ ℕ
2 reprval.m ⊢ φ → M ∈ ℤ
3 reprval.s ⊢ φ → S ∈ ℕ 0
4 reprss.1 ⊢ φ → B ⊆ A
5 nnex ⊢ ℕ ∈ V
6 5 a1i ⊢ φ → ℕ ∈ V
7 6 1 ssexd ⊢ φ → A ∈ V
8 mapss ⊢ A ∈ V ∧ B ⊆ A → B 0 ..^ S ⊆ A 0 ..^ S
9 7 4 8 syl2anc ⊢ φ → B 0 ..^ S ⊆ A 0 ..^ S
10 9 sselda ⊢ φ ∧ c ∈ B 0 ..^ S → c ∈ A 0 ..^ S
11 10 adantrr ⊢ φ ∧ c ∈ B 0 ..^ S ∧ ∑ a ∈ 0 ..^ S c ⁡ a = M → c ∈ A 0 ..^ S
12 11 rabss3d ⊢ φ → c ∈ B 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M ⊆ c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
13 4 1 sstrd ⊢ φ → B ⊆ ℕ
14 13 2 3 reprval ⊢ φ → B repr ⁡ S M = c ∈ B 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
15 1 2 3 reprval ⊢ φ → A repr ⁡ S M = c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
16 12 14 15 3sstr4d ⊢ φ → B repr ⁡ S M ⊆ A repr ⁡ S M