| Step | Hyp | Ref
| Expression |
| 1 | | nnex 12272 |
. . . . . . . . . . . . 13
⊢ ℕ
∈ V |
| 2 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℕ ∈
V) |
| 3 | | reprinfz1.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
| 4 | 2, 3 | ssexd 5324 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ V) |
| 5 | | ovex 7464 |
. . . . . . . . . . 11
⊢
(0..^𝑆) ∈
V |
| 6 | | elmapg 8879 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) |
| 7 | 4, 5, 6 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) |
| 8 | 7 | biimpa 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → 𝑐:(0..^𝑆)⟶𝐴) |
| 9 | 8 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → 𝑐:(0..^𝑆)⟶𝐴) |
| 10 | | elmapfn 8905 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) → 𝑐 Fn (0..^𝑆)) |
| 11 | 10 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → 𝑐 Fn (0..^𝑆)) |
| 12 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) ∧ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) |
| 13 | | reprinfz1.n |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 14 | 13 | nn0red 12588 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 15 | 14 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑁 ∈ ℝ) |
| 16 | 3 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝐴 ⊆ ℕ) |
| 17 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) |
| 18 | 7 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶𝐴)) |
| 19 | 17, 18 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑐:(0..^𝑆)⟶𝐴) |
| 20 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑏 ∈ (0..^𝑆)) |
| 21 | 19, 20 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐‘𝑏) ∈ 𝐴) |
| 22 | 16, 21 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐‘𝑏) ∈ ℕ) |
| 23 | 22 | nnred 12281 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐‘𝑏) ∈ ℝ) |
| 24 | | fzofi 14015 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0..^𝑆) ∈
Fin |
| 25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (0..^𝑆) ∈ Fin) |
| 26 | 3 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ) |
| 27 | 19 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ 𝐴) |
| 28 | 26, 27 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℕ) |
| 29 | 28 | nnred 12281 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℝ) |
| 30 | 25, 29 | fsumrecl 15770 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ ℝ) |
| 31 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ¬ (𝑐‘𝑏) ∈ (1...𝑁)) |
| 32 | 13 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 33 | 32 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑁 ∈ ℤ) |
| 34 | | fznn 13632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℤ → ((𝑐‘𝑏) ∈ (1...𝑁) ↔ ((𝑐‘𝑏) ∈ ℕ ∧ (𝑐‘𝑏) ≤ 𝑁))) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ((𝑐‘𝑏) ∈ (1...𝑁) ↔ ((𝑐‘𝑏) ∈ ℕ ∧ (𝑐‘𝑏) ≤ 𝑁))) |
| 36 | 22 | biantrurd 532 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ((𝑐‘𝑏) ≤ 𝑁 ↔ ((𝑐‘𝑏) ∈ ℕ ∧ (𝑐‘𝑏) ≤ 𝑁))) |
| 37 | 35, 36 | bitr4d 282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ((𝑐‘𝑏) ∈ (1...𝑁) ↔ (𝑐‘𝑏) ≤ 𝑁)) |
| 38 | 37 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (¬ (𝑐‘𝑏) ∈ (1...𝑁) ↔ ¬ (𝑐‘𝑏) ≤ 𝑁)) |
| 39 | 31, 38 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ¬ (𝑐‘𝑏) ≤ 𝑁) |
| 40 | 15, 23 | ltnled 11408 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑁 < (𝑐‘𝑏) ↔ ¬ (𝑐‘𝑏) ≤ 𝑁)) |
| 41 | 39, 40 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑁 < (𝑐‘𝑏)) |
| 42 | 23 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐‘𝑏) ∈ ℂ) |
| 43 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑏 → (𝑐‘𝑎) = (𝑐‘𝑏)) |
| 44 | 43 | sumsn 15782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 ∈ (0..^𝑆) ∧ (𝑐‘𝑏) ∈ ℂ) → Σ𝑎 ∈ {𝑏} (𝑐‘𝑎) = (𝑐‘𝑏)) |
| 45 | 20, 42, 44 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ {𝑏} (𝑐‘𝑎) = (𝑐‘𝑏)) |
| 46 | 28 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈
ℕ0) |
| 47 | | nn0ge0 12551 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐‘𝑎) ∈ ℕ0 → 0 ≤
(𝑐‘𝑎)) |
| 48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 0 ≤ (𝑐‘𝑎)) |
| 49 | | snssi 4808 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈ (0..^𝑆) → {𝑏} ⊆ (0..^𝑆)) |
| 50 | 49 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → {𝑏} ⊆ (0..^𝑆)) |
| 51 | 25, 29, 48, 50 | fsumless 15832 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ {𝑏} (𝑐‘𝑎) ≤ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
| 52 | 45, 51 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → (𝑐‘𝑏) ≤ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
| 53 | 15, 23, 30, 41, 52 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑁 < Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
| 54 | 15, 53 | ltned 11397 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → 𝑁 ≠ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎)) |
| 55 | 54 | necomd 2996 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ 𝑏 ∈ (0..^𝑆)) ∧ ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≠ 𝑁) |
| 56 | 55 | r19.29an 3158 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ≠ 𝑁) |
| 57 | 56 | neneqd 2945 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) |
| 58 | 57 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) ∧ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) → ¬ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) |
| 59 | 12, 58 | pm2.65da 817 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → ¬ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) |
| 60 | | dfral2 3099 |
. . . . . . . . . . . 12
⊢
(∀𝑏 ∈
(0..^𝑆)(𝑐‘𝑏) ∈ (1...𝑁) ↔ ¬ ∃𝑏 ∈ (0..^𝑆) ¬ (𝑐‘𝑏) ∈ (1...𝑁)) |
| 61 | 59, 60 | sylibr 234 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → ∀𝑏 ∈ (0..^𝑆)(𝑐‘𝑏) ∈ (1...𝑁)) |
| 62 | 43 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → ((𝑐‘𝑎) ∈ (1...𝑁) ↔ (𝑐‘𝑏) ∈ (1...𝑁))) |
| 63 | 62 | cbvralvw 3237 |
. . . . . . . . . . 11
⊢
(∀𝑎 ∈
(0..^𝑆)(𝑐‘𝑎) ∈ (1...𝑁) ↔ ∀𝑏 ∈ (0..^𝑆)(𝑐‘𝑏) ∈ (1...𝑁)) |
| 64 | 61, 63 | sylibr 234 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → ∀𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ (1...𝑁)) |
| 65 | 11, 64 | jca 511 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → (𝑐 Fn (0..^𝑆) ∧ ∀𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ (1...𝑁))) |
| 66 | | ffnfv 7139 |
. . . . . . . . 9
⊢ (𝑐:(0..^𝑆)⟶(1...𝑁) ↔ (𝑐 Fn (0..^𝑆) ∧ ∀𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) ∈ (1...𝑁))) |
| 67 | 65, 66 | sylibr 234 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → 𝑐:(0..^𝑆)⟶(1...𝑁)) |
| 68 | 9, 67 | jca 511 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → (𝑐:(0..^𝑆)⟶𝐴 ∧ 𝑐:(0..^𝑆)⟶(1...𝑁))) |
| 69 | | fin 6788 |
. . . . . . 7
⊢ (𝑐:(0..^𝑆)⟶(𝐴 ∩ (1...𝑁)) ↔ (𝑐:(0..^𝑆)⟶𝐴 ∧ 𝑐:(0..^𝑆)⟶(1...𝑁))) |
| 70 | 68, 69 | sylibr 234 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → 𝑐:(0..^𝑆)⟶(𝐴 ∩ (1...𝑁))) |
| 71 | | ovex 7464 |
. . . . . . . 8
⊢
(1...𝑁) ∈
V |
| 72 | 71 | inex2 5318 |
. . . . . . 7
⊢ (𝐴 ∩ (1...𝑁)) ∈ V |
| 73 | 72, 5 | elmap 8911 |
. . . . . 6
⊢ (𝑐 ∈ ((𝐴 ∩ (1...𝑁)) ↑m (0..^𝑆)) ↔ 𝑐:(0..^𝑆)⟶(𝐴 ∩ (1...𝑁))) |
| 74 | 70, 73 | sylibr 234 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁) → 𝑐 ∈ ((𝐴 ∩ (1...𝑁)) ↑m (0..^𝑆))) |
| 75 | 74 | anasss 466 |
. . . 4
⊢ ((𝜑 ∧ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁)) → 𝑐 ∈ ((𝐴 ∩ (1...𝑁)) ↑m (0..^𝑆))) |
| 76 | 75 | rabss3d 4081 |
. . 3
⊢ (𝜑 → {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁} ⊆ {𝑐 ∈ ((𝐴 ∩ (1...𝑁)) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁}) |
| 77 | | reprinfz1.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
| 78 | 3, 32, 77 | reprval 34625 |
. . 3
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁}) |
| 79 | | inss1 4237 |
. . . . . 6
⊢ (𝐴 ∩ (1...𝑁)) ⊆ 𝐴 |
| 80 | 79 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ (1...𝑁)) ⊆ 𝐴) |
| 81 | 80, 3 | sstrd 3994 |
. . . 4
⊢ (𝜑 → (𝐴 ∩ (1...𝑁)) ⊆ ℕ) |
| 82 | 81, 32, 77 | reprval 34625 |
. . 3
⊢ (𝜑 → ((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑁) = {𝑐 ∈ ((𝐴 ∩ (1...𝑁)) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑁}) |
| 83 | 76, 78, 82 | 3sstr4d 4039 |
. 2
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) ⊆ ((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑁)) |
| 84 | 3, 32, 77, 80 | reprss 34632 |
. 2
⊢ (𝜑 → ((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑁) ⊆ (𝐴(repr‘𝑆)𝑁)) |
| 85 | 83, 84 | eqssd 4001 |
1
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑁) = ((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑁)) |