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 ‘ 𝑆 ) 𝑁 ) )