| Step | Hyp | Ref
| Expression |
| 1 | | eqeq1 2741 |
. . . . 5
⊢ (𝑎 = 𝑡 → (𝑎 = (𝑏 ↾ (1...𝑁)) ↔ 𝑡 = (𝑏 ↾ (1...𝑁)))) |
| 2 | 1 | rexbidv 3179 |
. . . 4
⊢ (𝑎 = 𝑡 → (∃𝑏 ∈ 𝑆 𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏 ∈ 𝑆 𝑡 = (𝑏 ↾ (1...𝑁)))) |
| 3 | | reseq1 5991 |
. . . . . 6
⊢ (𝑏 = 𝑢 → (𝑏 ↾ (1...𝑁)) = (𝑢 ↾ (1...𝑁))) |
| 4 | 3 | eqeq2d 2748 |
. . . . 5
⊢ (𝑏 = 𝑢 → (𝑡 = (𝑏 ↾ (1...𝑁)) ↔ 𝑡 = (𝑢 ↾ (1...𝑁)))) |
| 5 | 4 | cbvrexvw 3238 |
. . . 4
⊢
(∃𝑏 ∈
𝑆 𝑡 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑢 ∈ 𝑆 𝑡 = (𝑢 ↾ (1...𝑁))) |
| 6 | 2, 5 | bitrdi 287 |
. . 3
⊢ (𝑎 = 𝑡 → (∃𝑏 ∈ 𝑆 𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑢 ∈ 𝑆 𝑡 = (𝑢 ↾ (1...𝑁)))) |
| 7 | 6 | cbvabv 2812 |
. 2
⊢ {𝑎 ∣ ∃𝑏 ∈ 𝑆 𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑡 ∣ ∃𝑢 ∈ 𝑆 𝑡 = (𝑢 ↾ (1...𝑁))} |
| 8 | | rexeq 3322 |
. . . . . 6
⊢ (𝑆 = {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)} → (∃𝑏 ∈ 𝑆 𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏 ∈ {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}𝑎 = (𝑏 ↾ (1...𝑁)))) |
| 9 | 8 | abbidv 2808 |
. . . . 5
⊢ (𝑆 = {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)} → {𝑎 ∣ ∃𝑏 ∈ 𝑆 𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑏 ∈ {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}𝑎 = (𝑏 ↾ (1...𝑁))}) |
| 10 | 9 | adantl 481 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) ∧ 𝑆 = {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}) → {𝑎 ∣ ∃𝑏 ∈ 𝑆 𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑏 ∈ {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}𝑎 = (𝑏 ↾ (1...𝑁))}) |
| 11 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑏 → (𝑑 = (𝑒 ↾ (1...𝑀)) ↔ 𝑏 = (𝑒 ↾ (1...𝑀)))) |
| 12 | 11 | anbi1d 631 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑏 → ((𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ↔ (𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0))) |
| 13 | 12 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑑 = 𝑏 → (∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ↔ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0))) |
| 14 | 13 | rexab 3700 |
. . . . . . . 8
⊢
(∃𝑏 ∈
{𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏(∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) |
| 15 | | r19.41v 3189 |
. . . . . . . . . 10
⊢
(∃𝑒 ∈
(ℕ0 ↑m ℕ)((𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ (∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) |
| 16 | 15 | exbii 1848 |
. . . . . . . . 9
⊢
(∃𝑏∃𝑒 ∈ (ℕ0
↑m ℕ)((𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ∃𝑏(∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) |
| 17 | | rexcom4 3288 |
. . . . . . . . . 10
⊢
(∃𝑒 ∈
(ℕ0 ↑m ℕ)∃𝑏((𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ∃𝑏∃𝑒 ∈ (ℕ0
↑m ℕ)((𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) |
| 18 | | anass 468 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ (𝑏 = (𝑒 ↾ (1...𝑀)) ∧ ((𝑐‘𝑒) = 0 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))) |
| 19 | 18 | exbii 1848 |
. . . . . . . . . . . . 13
⊢
(∃𝑏((𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ∃𝑏(𝑏 = (𝑒 ↾ (1...𝑀)) ∧ ((𝑐‘𝑒) = 0 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))) |
| 20 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑒 ∈ V |
| 21 | 20 | resex 6047 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ↾ (1...𝑀)) ∈ V |
| 22 | | reseq1 5991 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑒 ↾ (1...𝑀)) → (𝑏 ↾ (1...𝑁)) = ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁))) |
| 23 | 22 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑒 ↾ (1...𝑀)) → (𝑎 = (𝑏 ↾ (1...𝑁)) ↔ 𝑎 = ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁)))) |
| 24 | 23 | anbi2d 630 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑒 ↾ (1...𝑀)) → (((𝑐‘𝑒) = 0 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ((𝑐‘𝑒) = 0 ∧ 𝑎 = ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁))))) |
| 25 | 21, 24 | ceqsexv 3532 |
. . . . . . . . . . . . 13
⊢
(∃𝑏(𝑏 = (𝑒 ↾ (1...𝑀)) ∧ ((𝑐‘𝑒) = 0 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) ↔ ((𝑐‘𝑒) = 0 ∧ 𝑎 = ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁)))) |
| 26 | 19, 25 | bitri 275 |
. . . . . . . . . . . 12
⊢
(∃𝑏((𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ((𝑐‘𝑒) = 0 ∧ 𝑎 = ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁)))) |
| 27 | | ancom 460 |
. . . . . . . . . . . . 13
⊢ (((𝑐‘𝑒) = 0 ∧ 𝑎 = ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁))) ↔ (𝑎 = ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0)) |
| 28 | | simpl2 1193 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) → 𝑀 ∈
(ℤ≥‘𝑁)) |
| 29 | | fzss2 13604 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...𝑀)) |
| 30 | | resabs1 6024 |
. . . . . . . . . . . . . . . 16
⊢
((1...𝑁) ⊆
(1...𝑀) → ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁)) = (𝑒 ↾ (1...𝑁))) |
| 31 | 28, 29, 30 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) →
((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁)) = (𝑒 ↾ (1...𝑁))) |
| 32 | 31 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) → (𝑎 = ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁)) ↔ 𝑎 = (𝑒 ↾ (1...𝑁)))) |
| 33 | 32 | anbi1d 631 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) →
((𝑎 = ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0) ↔ (𝑎 = (𝑒 ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0))) |
| 34 | 27, 33 | bitrid 283 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) →
(((𝑐‘𝑒) = 0 ∧ 𝑎 = ((𝑒 ↾ (1...𝑀)) ↾ (1...𝑁))) ↔ (𝑎 = (𝑒 ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0))) |
| 35 | 26, 34 | bitrid 283 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) →
(∃𝑏((𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ (𝑎 = (𝑒 ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0))) |
| 36 | 35 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) →
(∃𝑒 ∈
(ℕ0 ↑m ℕ)∃𝑏((𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑎 = (𝑒 ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0))) |
| 37 | 17, 36 | bitr3id 285 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) →
(∃𝑏∃𝑒 ∈ (ℕ0
↑m ℕ)((𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑎 = (𝑒 ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0))) |
| 38 | 16, 37 | bitr3id 285 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) →
(∃𝑏(∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑏 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0) ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑎 = (𝑒 ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0))) |
| 39 | 14, 38 | bitrid 283 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) →
(∃𝑏 ∈ {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑎 = (𝑒 ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0))) |
| 40 | 39 | abbidv 2808 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) → {𝑎 ∣ ∃𝑏 ∈ {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑎 = (𝑒 ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0)}) |
| 41 | | eldioph3 42777 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑐 ∈
(mzPoly‘ℕ)) → {𝑎 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑎 = (𝑒 ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0)} ∈ (Dioph‘𝑁)) |
| 42 | 41 | 3ad2antl1 1186 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) → {𝑎 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑎 = (𝑒 ↾ (1...𝑁)) ∧ (𝑐‘𝑒) = 0)} ∈ (Dioph‘𝑁)) |
| 43 | 40, 42 | eqeltrd 2841 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) → {𝑎 ∣ ∃𝑏 ∈ {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}𝑎 = (𝑏 ↾ (1...𝑁))} ∈ (Dioph‘𝑁)) |
| 44 | 43 | adantr 480 |
. . . 4
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) ∧ 𝑆 = {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}) → {𝑎 ∣ ∃𝑏 ∈ {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}𝑎 = (𝑏 ↾ (1...𝑁))} ∈ (Dioph‘𝑁)) |
| 45 | 10, 44 | eqeltrd 2841 |
. . 3
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) ∧ 𝑐 ∈ (mzPoly‘ℕ)) ∧ 𝑆 = {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}) → {𝑎 ∣ ∃𝑏 ∈ 𝑆 𝑎 = (𝑏 ↾ (1...𝑁))} ∈ (Dioph‘𝑁)) |
| 46 | | eldioph3b 42776 |
. . . . 5
⊢ (𝑆 ∈ (Dioph‘𝑀) ↔ (𝑀 ∈ ℕ0 ∧
∃𝑐 ∈
(mzPoly‘ℕ)𝑆 =
{𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)})) |
| 47 | 46 | simprbi 496 |
. . . 4
⊢ (𝑆 ∈ (Dioph‘𝑀) → ∃𝑐 ∈
(mzPoly‘ℕ)𝑆 =
{𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}) |
| 48 | 47 | 3ad2ant3 1136 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) → ∃𝑐 ∈ (mzPoly‘ℕ)𝑆 = {𝑑 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑑 = (𝑒 ↾ (1...𝑀)) ∧ (𝑐‘𝑒) = 0)}) |
| 49 | 45, 48 | r19.29a 3162 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) → {𝑎 ∣ ∃𝑏 ∈ 𝑆 𝑎 = (𝑏 ↾ (1...𝑁))} ∈ (Dioph‘𝑁)) |
| 50 | 7, 49 | eqeltrrid 2846 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑆 ∈ (Dioph‘𝑀)) → {𝑡 ∣ ∃𝑢 ∈ 𝑆 𝑡 = (𝑢 ↾ (1...𝑁))} ∈ (Dioph‘𝑁)) |