Step | Hyp | Ref
| Expression |
1 | | nnex 11979 |
. . . . . . . . . . . . 13
⊢ ℕ
∈ V |
2 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℕ ∈
V) |
3 | | reprinfz1.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
4 | 2, 3 | ssexd 5248 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ V) |
5 | | ovex 7308 |
. . . . . . . . . . 11
⊢
(0..^𝑆) ∈
V |
6 | | elmapg 8628 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) |
7 | 4, 5, 6 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) |
8 | 7 | biimpa 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐:(0..^𝑆)⟶𝐴) |
9 | 8 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → 𝑐:(0..^𝑆)⟶𝐴) |
10 | | elmapfn 8653 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) → 𝑐 Fn (0..^𝑆)) |
11 | 10 | ad2antlr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → 𝑐 Fn (0..^𝑆)) |
12 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) ∧ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) |
13 | | reprinfz1.n |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
14 | 13 | nn0red 12294 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℝ) |
15 | 14 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑁 ∈ ℝ) |
16 | 3 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝐴 ⊆ ℕ) |
17 | | simpllr 773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) |
18 | 7 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) |
19 | 17, 18 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑐:(0..^𝑆)⟶𝐴) |
20 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑏 ∈ (0..^𝑆)) |
21 | 19, 20 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐‘𝑏) ∈ 𝐴) |
22 | 16, 21 | sseldd 3922 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐‘𝑏) ∈ ℕ) |
23 | 22 | nnred 11988 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐‘𝑏) ∈ ℝ) |
24 | | fzofi 13694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0..^𝑆) ∈
Fin |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (0..^𝑆) ∈ Fin) |
26 | 3 | ad4antr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ) |
27 | 19 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ 𝐴) |
28 | 26, 27 | sseldd 3922 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℕ) |
29 | 28 | nnred 11988 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℝ) |
30 | 25, 29 | fsumrecl 15446 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ ℝ) |
31 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ¬ (𝑐‘𝑏) ∈ (1...𝑁)) |
32 | 13 | nn0zd 12424 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑁 ∈ ℤ) |
33 | 32 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑁 ∈ ℤ) |
34 | | fznn 13324 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℤ → ((𝑐‘𝑏) ∈ (1...𝑁) ↔ ((𝑐‘𝑏) ∈ ℕ ∧ (𝑐‘𝑏) ≤ 𝑁))) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ((𝑐‘𝑏) ∈ (1...𝑁) ↔ ((𝑐‘𝑏) ∈ ℕ ∧ (𝑐‘𝑏) ≤ 𝑁))) |
36 | 22 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ((𝑐‘𝑏) ≤ 𝑁 ↔ ((𝑐‘𝑏) ∈ ℕ ∧ (𝑐‘𝑏) ≤ 𝑁))) |
37 | 35, 36 | bitr4d 281 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ((𝑐‘𝑏) ∈ (1...𝑁) ↔ (𝑐‘𝑏) ≤ 𝑁)) |
38 | 37 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (¬ (𝑐‘𝑏) ∈ (1...𝑁) ↔ ¬ (𝑐‘𝑏) ≤ 𝑁)) |
39 | 31, 38 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ¬ (𝑐‘𝑏) ≤ 𝑁) |
40 | 15, 23 | ltnled 11122 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑁 < (𝑐‘𝑏) ↔ ¬ (𝑐‘𝑏) ≤ 𝑁)) |
41 | 39, 40 | mpbird 256 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑁 < (𝑐‘𝑏)) |
42 | 23 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐‘𝑏) ∈ ℂ) |
43 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑏 → (𝑐‘𝑎) = (𝑐‘𝑏)) |
44 | 43 | sumsn 15458 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 ∈ (0..^𝑆) ∧ (𝑐‘𝑏) ∈ ℂ) → Σ𝑎 ∈ {𝑏} (𝑐‘𝑎) = (𝑐‘𝑏)) |
45 | 20, 42, 44 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ {𝑏} (𝑐‘𝑎) = (𝑐‘𝑏)) |
46 | 28 | nnnn0d 12293 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈
ℕ0) |
47 | | nn0ge0 12258 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐‘𝑎) ∈ ℕ0 → 0 ≤
(𝑐‘𝑎)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 0 ≤ (𝑐‘𝑎)) |
49 | | snssi 4741 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈ (0..^𝑆) → {𝑏} ⊆ (0..^𝑆)) |
50 | 49 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → {𝑏} ⊆ (0..^𝑆)) |
51 | 25, 29, 48, 50 | fsumless 15508 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ {𝑏} (𝑐‘𝑎) ≤ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
52 | 45, 51 | eqbrtrrd 5098 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐‘𝑏) ≤ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
53 | 15, 23, 30, 41, 52 | ltletrd 11135 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑁 < Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
54 | 15, 53 | ltned 11111 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑁 ≠ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
55 | 54 | necomd 2999 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≠ 𝑁) |
56 | 55 | r19.29an 3217 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≠ 𝑁) |
57 | 56 | neneqd 2948 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) |
58 | 57 | adantlr 712 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) ∧ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) |
59 | 12, 58 | pm2.65da 814 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → ¬ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) |
60 | | dfral2 3168 |
. . . . . . . . . . . 12
⊢
(∀𝑏 ∈
(0..^𝑆)(𝑐‘𝑏) ∈ (1...𝑁) ↔ ¬ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) |
61 | 59, 60 | sylibr 233 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → ∀𝑏 ∈ (0..^𝑆)(𝑐‘𝑏) ∈ (1...𝑁)) |
62 | 43 | eleq1d 2823 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → ((𝑐‘𝑎) ∈ (1...𝑁) ↔ (𝑐‘𝑏) ∈ (1...𝑁))) |
63 | 62 | cbvralvw 3383 |
. . . . . . . . . . 11
⊢
(∀𝑎 ∈
(0..^𝑆)(𝑐‘𝑎) ∈ (1...𝑁) ↔ ∀𝑏 ∈ (0..^𝑆)(𝑐‘𝑏) ∈ (1...𝑁)) |
64 | 61, 63 | sylibr 233 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → ∀𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ (1...𝑁)) |
65 | 11, 64 | jca 512 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → (𝑐 Fn (0..^𝑆) ∧ ∀𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ (1...𝑁))) |
66 | | ffnfv 6992 |
. . . . . . . . 9
⊢ (𝑐:(0..^𝑆)⟶(1...𝑁) ↔ (𝑐 Fn (0..^𝑆) ∧ ∀𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ (1...𝑁))) |
67 | 65, 66 | sylibr 233 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → 𝑐:(0..^𝑆)⟶(1...𝑁)) |
68 | 9, 67 | jca 512 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → (𝑐:(0..^𝑆)⟶𝐴 ∧ 𝑐:(0..^𝑆)⟶(1...𝑁))) |
69 | | fin 6654 |
. . . . . . 7
⊢ (𝑐:(0..^𝑆)⟶(𝐴 ∩ (1...𝑁)) ↔ (𝑐:(0..^𝑆)⟶𝐴 ∧ 𝑐:(0..^𝑆)⟶(1...𝑁))) |
70 | 68, 69 | sylibr 233 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → 𝑐:(0..^𝑆)⟶(𝐴 ∩ (1...𝑁))) |
71 | | ovex 7308 |
. . . . . . . 8
⊢
(1...𝑁) ∈
V |
72 | 71 | inex2 5242 |
. . . . . . 7
⊢ (𝐴 ∩ (1...𝑁)) ∈ V |
73 | 72, 5 | elmap 8659 |
. . . . . 6
⊢ (𝑐 ∈ ((𝐴 ∩ (1...𝑁)) ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶(𝐴 ∩ (1...𝑁))) |
74 | 70, 73 | sylibr 233 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → 𝑐 ∈ ((𝐴 ∩ (1...𝑁)) ↑m (0..^𝑆))) |
75 | 74 | anasss 467 |
. . . 4
⊢ ((𝜑 ∧ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁)) → 𝑐 ∈ ((𝐴 ∩ (1...𝑁)) ↑m (0..^𝑆))) |
76 | 75 | rabss3d 30861 |
. . 3
⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁} ⊆ {𝑐 ∈ ((𝐴 ∩ (1...𝑁)) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁}) |
77 | | reprinfz1.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
78 | 3, 32, 77 | reprval 32590 |
. . 3
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁}) |
79 | | inss1 4162 |
. . . . . 6
⊢ (𝐴 ∩ (1...𝑁)) ⊆ 𝐴 |
80 | 79 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ (1...𝑁)) ⊆ 𝐴) |
81 | 80, 3 | sstrd 3931 |
. . . 4
⊢ (𝜑 → (𝐴 ∩ (1...𝑁)) ⊆ ℕ) |
82 | 81, 32, 77 | reprval 32590 |
. . 3
⊢ (𝜑 → ((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑁) = {𝑐 ∈ ((𝐴 ∩ (1...𝑁)) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁}) |
83 | 76, 78, 82 | 3sstr4d 3968 |
. 2
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) ⊆ ((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑁)) |
84 | 3, 32, 77, 80 | reprss 32597 |
. 2
⊢ (𝜑 → ((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑁) ⊆ (𝐴(repr‘𝑆)𝑁)) |
85 | 83, 84 | eqssd 3938 |
1
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) = ((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑁)) |