Metamath Proof Explorer


Theorem reprinfz1

Description: For the representation of N , it is sufficient to consider nonnegative integers up to N . Remark of Nathanson p. 123 (Contributed by Thierry Arnoux, 13-Dec-2021)

Ref Expression
Hypotheses reprinfz1.n ( 𝜑𝑁 ∈ ℕ0 )
reprinfz1.s ( 𝜑𝑆 ∈ ℕ0 )
reprinfz1.a ( 𝜑𝐴 ⊆ ℕ )
Assertion reprinfz1 ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) = ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑁 ) )

Proof

Step Hyp Ref Expression
1 reprinfz1.n ( 𝜑𝑁 ∈ ℕ0 )
2 reprinfz1.s ( 𝜑𝑆 ∈ ℕ0 )
3 reprinfz1.a ( 𝜑𝐴 ⊆ ℕ )
4 nnex ℕ ∈ V
5 4 a1i ( 𝜑 → ℕ ∈ V )
6 5 3 ssexd ( 𝜑𝐴 ∈ V )
7 ovex ( 0 ..^ 𝑆 ) ∈ V
8 elmapg ( ( 𝐴 ∈ V ∧ ( 0 ..^ 𝑆 ) ∈ V ) → ( 𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ↔ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
9 6 7 8 sylancl ( 𝜑 → ( 𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ↔ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
10 9 biimpa ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
11 10 adantr ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
12 elmapfn ( 𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) → 𝑐 Fn ( 0 ..^ 𝑆 ) )
13 12 ad2antlr ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) → 𝑐 Fn ( 0 ..^ 𝑆 ) )
14 simplr ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) ∧ ∃ 𝑏 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 )
15 1 nn0red ( 𝜑𝑁 ∈ ℝ )
16 15 ad3antrrr ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
17 3 ad3antrrr ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → 𝐴 ⊆ ℕ )
18 simpllr ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → 𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) )
19 9 ad3antrrr ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ↔ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 ) )
20 18 19 mpbid ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
21 simplr ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ( 0 ..^ 𝑆 ) )
22 20 21 ffvelrnd ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑐𝑏 ) ∈ 𝐴 )
23 17 22 sseldd ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑐𝑏 ) ∈ ℕ )
24 23 nnred ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑐𝑏 ) ∈ ℝ )
25 fzofi ( 0 ..^ 𝑆 ) ∈ Fin
26 25 a1i ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
27 3 ad4antr ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℕ )
28 20 ffvelrnda ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐𝑎 ) ∈ 𝐴 )
29 27 28 sseldd ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐𝑎 ) ∈ ℕ )
30 29 nnred ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐𝑎 ) ∈ ℝ )
31 26 30 fsumrecl ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) ∈ ℝ )
32 simpr ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) )
33 1 nn0zd ( 𝜑𝑁 ∈ ℤ )
34 33 ad3antrrr ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
35 fznn ( 𝑁 ∈ ℤ → ( ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑐𝑏 ) ∈ ℕ ∧ ( 𝑐𝑏 ) ≤ 𝑁 ) ) )
36 34 35 syl ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑐𝑏 ) ∈ ℕ ∧ ( 𝑐𝑏 ) ≤ 𝑁 ) ) )
37 23 biantrurd ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑐𝑏 ) ≤ 𝑁 ↔ ( ( 𝑐𝑏 ) ∈ ℕ ∧ ( 𝑐𝑏 ) ≤ 𝑁 ) ) )
38 36 37 bitr4d ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ↔ ( 𝑐𝑏 ) ≤ 𝑁 ) )
39 38 notbid ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ↔ ¬ ( 𝑐𝑏 ) ≤ 𝑁 ) )
40 32 39 mpbid ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ¬ ( 𝑐𝑏 ) ≤ 𝑁 )
41 16 24 ltnled ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑁 < ( 𝑐𝑏 ) ↔ ¬ ( 𝑐𝑏 ) ≤ 𝑁 ) )
42 40 41 mpbird ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 < ( 𝑐𝑏 ) )
43 24 recnd ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑐𝑏 ) ∈ ℂ )
44 fveq2 ( 𝑎 = 𝑏 → ( 𝑐𝑎 ) = ( 𝑐𝑏 ) )
45 44 sumsn ( ( 𝑏 ∈ ( 0 ..^ 𝑆 ) ∧ ( 𝑐𝑏 ) ∈ ℂ ) → Σ 𝑎 ∈ { 𝑏 } ( 𝑐𝑎 ) = ( 𝑐𝑏 ) )
46 21 43 45 syl2anc ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → Σ 𝑎 ∈ { 𝑏 } ( 𝑐𝑎 ) = ( 𝑐𝑏 ) )
47 29 nnnn0d ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐𝑎 ) ∈ ℕ0 )
48 nn0ge0 ( ( 𝑐𝑎 ) ∈ ℕ0 → 0 ≤ ( 𝑐𝑎 ) )
49 47 48 syl ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 0 ≤ ( 𝑐𝑎 ) )
50 snssi ( 𝑏 ∈ ( 0 ..^ 𝑆 ) → { 𝑏 } ⊆ ( 0 ..^ 𝑆 ) )
51 50 ad2antlr ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → { 𝑏 } ⊆ ( 0 ..^ 𝑆 ) )
52 26 30 49 51 fsumless ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → Σ 𝑎 ∈ { 𝑏 } ( 𝑐𝑎 ) ≤ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) )
53 46 52 eqbrtrrd ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑐𝑏 ) ≤ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) )
54 16 24 31 42 53 ltletrd ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 < Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) )
55 16 54 ltned ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → 𝑁 ≠ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) )
56 55 necomd ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ 𝑏 ∈ ( 0 ..^ 𝑆 ) ) ∧ ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) ≠ 𝑁 )
57 56 r19.29an ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ ∃ 𝑏 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) ≠ 𝑁 )
58 57 neneqd ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ ∃ 𝑏 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ¬ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 )
59 58 adantlr ( ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) ∧ ∃ 𝑏 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) → ¬ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 )
60 14 59 pm2.65da ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) → ¬ ∃ 𝑏 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) )
61 dfral2 ( ∀ 𝑏 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ↔ ¬ ∃ 𝑏 ∈ ( 0 ..^ 𝑆 ) ¬ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) )
62 60 61 sylibr ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) → ∀ 𝑏 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) )
63 44 eleq1d ( 𝑎 = 𝑏 → ( ( 𝑐𝑎 ) ∈ ( 1 ... 𝑁 ) ↔ ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) ) )
64 63 cbvralvw ( ∀ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) ∈ ( 1 ... 𝑁 ) ↔ ∀ 𝑏 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑏 ) ∈ ( 1 ... 𝑁 ) )
65 62 64 sylibr ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) → ∀ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) ∈ ( 1 ... 𝑁 ) )
66 13 65 jca ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) → ( 𝑐 Fn ( 0 ..^ 𝑆 ) ∧ ∀ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) ∈ ( 1 ... 𝑁 ) ) )
67 ffnfv ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 1 ... 𝑁 ) ↔ ( 𝑐 Fn ( 0 ..^ 𝑆 ) ∧ ∀ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) ∈ ( 1 ... 𝑁 ) ) )
68 66 67 sylibr ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 1 ... 𝑁 ) )
69 11 68 jca ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) → ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 1 ... 𝑁 ) ) )
70 fin ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ↔ ( 𝑐 : ( 0 ..^ 𝑆 ) ⟶ 𝐴𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 1 ... 𝑁 ) ) )
71 69 70 sylibr ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) )
72 ovex ( 1 ... 𝑁 ) ∈ V
73 72 inex2 ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ∈ V
74 73 7 elmap ( 𝑐 ∈ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ↑m ( 0 ..^ 𝑆 ) ) ↔ 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) )
75 71 74 sylibr ( ( ( 𝜑𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) → 𝑐 ∈ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ↑m ( 0 ..^ 𝑆 ) ) )
76 75 anasss ( ( 𝜑 ∧ ( 𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 ) ) → 𝑐 ∈ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ↑m ( 0 ..^ 𝑆 ) ) )
77 76 rabss3d ( 𝜑 → { 𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 } ⊆ { 𝑐 ∈ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 } )
78 3 33 2 reprval ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) = { 𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 } )
79 inss1 ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ⊆ 𝐴
80 79 a1i ( 𝜑 → ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ⊆ 𝐴 )
81 80 3 sstrd ( 𝜑 → ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ⊆ ℕ )
82 81 33 2 reprval ( 𝜑 → ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑁 ) = { 𝑐 ∈ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑁 } )
83 77 78 82 3sstr4d ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) ⊆ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑁 ) )
84 3 33 2 80 reprss ( 𝜑 → ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑁 ) ⊆ ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) )
85 83 84 eqssd ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) = ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑁 ) )