| Step | Hyp | Ref
| Expression |
| 1 | | df-dioph 42767 |
. . . 4
⊢ Dioph =
(𝑛 ∈
ℕ0 ↦ ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)})) |
| 2 | 1 | dmmptss 6261 |
. . 3
⊢ dom Dioph
⊆ ℕ0 |
| 3 | | elfvdm 6943 |
. . 3
⊢ (𝐷 ∈ (Dioph‘𝑁) → 𝑁 ∈ dom Dioph) |
| 4 | 2, 3 | sselid 3981 |
. 2
⊢ (𝐷 ∈ (Dioph‘𝑁) → 𝑁 ∈
ℕ0) |
| 5 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑁)) |
| 6 | | eqidd 2738 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (mzPoly‘(1...𝑘)) = (mzPoly‘(1...𝑘))) |
| 7 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁)) |
| 8 | 7 | reseq2d 5997 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → (𝑢 ↾ (1...𝑛)) = (𝑢 ↾ (1...𝑁))) |
| 9 | 8 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (𝑡 = (𝑢 ↾ (1...𝑛)) ↔ 𝑡 = (𝑢 ↾ (1...𝑁)))) |
| 10 | 9 | anbi1d 631 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0) ↔ (𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0))) |
| 11 | 10 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0) ↔ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0))) |
| 12 | 11 | abbidv 2808 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)} = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) |
| 13 | 5, 6, 12 | mpoeq123dv 7508 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}) = (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
| 14 | 13 | rneqd 5949 |
. . . . 5
⊢ (𝑛 = 𝑁 → ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}) = ran (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
| 15 | | ovex 7464 |
. . . . . . 7
⊢
(ℕ0 ↑m (1...𝑁)) ∈ V |
| 16 | 15 | pwex 5380 |
. . . . . 6
⊢ 𝒫
(ℕ0 ↑m (1...𝑁)) ∈ V |
| 17 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) = (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) |
| 18 | 17 | rnmpo 7566 |
. . . . . . 7
⊢ ran
(𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) = {𝑑 ∣ ∃𝑘 ∈ (ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}} |
| 19 | | elmapi 8889 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (ℕ0
↑m (1...𝑘))
→ 𝑢:(1...𝑘)⟶ℕ0) |
| 20 | | fzss2 13604 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...𝑘)) |
| 21 | | fssres 6774 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢:(1...𝑘)⟶ℕ0 ∧ (1...𝑁) ⊆ (1...𝑘)) → (𝑢 ↾ (1...𝑁)):(1...𝑁)⟶ℕ0) |
| 22 | 19, 20, 21 | syl2anr 597 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈
(ℤ≥‘𝑁) ∧ 𝑢 ∈ (ℕ0
↑m (1...𝑘))) → (𝑢 ↾ (1...𝑁)):(1...𝑁)⟶ℕ0) |
| 23 | | nn0ex 12532 |
. . . . . . . . . . . . . . . . 17
⊢
ℕ0 ∈ V |
| 24 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑁) ∈
V |
| 25 | 23, 24 | elmap 8911 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑m (1...𝑁))
↔ (𝑢 ↾
(1...𝑁)):(1...𝑁)⟶ℕ0) |
| 26 | 22, 25 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈
(ℤ≥‘𝑁) ∧ 𝑢 ∈ (ℕ0
↑m (1...𝑘))) → (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑m (1...𝑁))) |
| 27 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → (𝑡 ∈ (ℕ0
↑m (1...𝑁))
↔ (𝑢 ↾
(1...𝑁)) ∈
(ℕ0 ↑m (1...𝑁)))) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → (𝑡 ∈ (ℕ0
↑m (1...𝑁))
↔ (𝑢 ↾
(1...𝑁)) ∈
(ℕ0 ↑m (1...𝑁)))) |
| 29 | 26, 28 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘𝑁) ∧ 𝑢 ∈ (ℕ0
↑m (1...𝑘))) → ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → 𝑡 ∈ (ℕ0
↑m (1...𝑁)))) |
| 30 | 29 | rexlimdva 3155 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → 𝑡 ∈ (ℕ0
↑m (1...𝑁)))) |
| 31 | 30 | abssdv 4068 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ⊆ (ℕ0
↑m (1...𝑁))) |
| 32 | 15 | elpw2 5334 |
. . . . . . . . . . . 12
⊢ ({𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ 𝒫 (ℕ0
↑m (1...𝑁))
↔ {𝑡 ∣
∃𝑢 ∈
(ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ⊆ (ℕ0
↑m (1...𝑁))) |
| 33 | 31, 32 | sylibr 234 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ 𝒫 (ℕ0
↑m (1...𝑁))) |
| 34 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → (𝑑 ∈ 𝒫 (ℕ0
↑m (1...𝑁))
↔ {𝑡 ∣
∃𝑢 ∈
(ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ 𝒫 (ℕ0
↑m (1...𝑁)))) |
| 35 | 33, 34 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → 𝑑 ∈ 𝒫 (ℕ0
↑m (1...𝑁)))) |
| 36 | 35 | rexlimdvw 3160 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → 𝑑 ∈ 𝒫 (ℕ0
↑m (1...𝑁)))) |
| 37 | 36 | rexlimiv 3148 |
. . . . . . . 8
⊢
(∃𝑘 ∈
(ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → 𝑑 ∈ 𝒫 (ℕ0
↑m (1...𝑁))) |
| 38 | 37 | abssi 4070 |
. . . . . . 7
⊢ {𝑑 ∣ ∃𝑘 ∈
(ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}} ⊆ 𝒫
(ℕ0 ↑m (1...𝑁)) |
| 39 | 18, 38 | eqsstri 4030 |
. . . . . 6
⊢ ran
(𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) ⊆ 𝒫
(ℕ0 ↑m (1...𝑁)) |
| 40 | 16, 39 | ssexi 5322 |
. . . . 5
⊢ ran
(𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) ∈ V |
| 41 | 14, 1, 40 | fvmpt 7016 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (Dioph‘𝑁) =
ran (𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
| 42 | 41 | eleq2d 2827 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐷 ∈
(Dioph‘𝑁) ↔
𝐷 ∈ ran (𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}))) |
| 43 | | ovex 7464 |
. . . . . 6
⊢
(ℕ0 ↑m (1...𝑘)) ∈ V |
| 44 | 43 | abrexex 7987 |
. . . . 5
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))𝑡 = (𝑢 ↾ (1...𝑁))} ∈ V |
| 45 | | simpl 482 |
. . . . . . 7
⊢ ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → 𝑡 = (𝑢 ↾ (1...𝑁))) |
| 46 | 45 | reximi 3084 |
. . . . . 6
⊢
(∃𝑢 ∈
(ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))𝑡 = (𝑢 ↾ (1...𝑁))) |
| 47 | 46 | ss2abi 4067 |
. . . . 5
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ⊆ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))𝑡 = (𝑢 ↾ (1...𝑁))} |
| 48 | 44, 47 | ssexi 5322 |
. . . 4
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ V |
| 49 | 17, 48 | elrnmpo 7569 |
. . 3
⊢ (𝐷 ∈ ran (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) ↔ ∃𝑘 ∈ (ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝐷 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) |
| 50 | 42, 49 | bitrdi 287 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐷 ∈
(Dioph‘𝑁) ↔
∃𝑘 ∈
(ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝐷 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
| 51 | 4, 50 | biadanii 822 |
1
⊢ (𝐷 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧
∃𝑘 ∈
(ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝐷 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |