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