Step | Hyp | Ref
| Expression |
1 | | df-dioph 36337 |
. . . 4
⊢ Dioph =
(𝑛 ∈
ℕ0 ↦ ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)})) |
2 | 1 | dmmptss 5548 |
. . 3
⊢ dom Dioph
⊆ ℕ0 |
3 | | elfvdm 6130 |
. . 3
⊢ (𝐷 ∈ (Dioph‘𝑁) → 𝑁 ∈ dom Dioph) |
4 | 2, 3 | sseldi 3566 |
. 2
⊢ (𝐷 ∈ (Dioph‘𝑁) → 𝑁 ∈
ℕ0) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑁)) |
6 | | eqidd 2611 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (mzPoly‘(1...𝑘)) = (mzPoly‘(1...𝑘))) |
7 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁)) |
8 | 7 | reseq2d 5317 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → (𝑢 ↾ (1...𝑛)) = (𝑢 ↾ (1...𝑁))) |
9 | 8 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (𝑡 = (𝑢 ↾ (1...𝑛)) ↔ 𝑡 = (𝑢 ↾ (1...𝑁)))) |
10 | 9 | anbi1d 737 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0) ↔ (𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0))) |
11 | 10 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0) ↔ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0))) |
12 | 11 | abbidv 2728 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)} = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) |
13 | 5, 6, 12 | mpt2eq123dv 6615 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}) = (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
14 | 13 | rneqd 5274 |
. . . . 5
⊢ (𝑛 = 𝑁 → ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}) = ran (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
15 | | ovex 6577 |
. . . . . . 7
⊢
(ℕ0 ↑𝑚 (1...𝑁)) ∈ V |
16 | 15 | pwex 4774 |
. . . . . 6
⊢ 𝒫
(ℕ0 ↑𝑚 (1...𝑁)) ∈ V |
17 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) = (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) |
18 | 17 | rnmpt2 6668 |
. . . . . . 7
⊢ ran
(𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) = {𝑑 ∣ ∃𝑘 ∈ (ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}} |
19 | | elmapi 7765 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘)) → 𝑢:(1...𝑘)⟶ℕ0) |
20 | | fzss2 12252 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...𝑘)) |
21 | | fssres 5983 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢:(1...𝑘)⟶ℕ0 ∧ (1...𝑁) ⊆ (1...𝑘)) → (𝑢 ↾ (1...𝑁)):(1...𝑁)⟶ℕ0) |
22 | 19, 20, 21 | syl2anr 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈
(ℤ≥‘𝑁) ∧ 𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))) → (𝑢 ↾ (1...𝑁)):(1...𝑁)⟶ℕ0) |
23 | | nn0ex 11175 |
. . . . . . . . . . . . . . . . 17
⊢
ℕ0 ∈ V |
24 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑁) ∈
V |
25 | 23, 24 | elmap 7772 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁)) ↔ (𝑢 ↾ (1...𝑁)):(1...𝑁)⟶ℕ0) |
26 | 22, 25 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈
(ℤ≥‘𝑁) ∧ 𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))) → (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
27 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ↔ (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁)))) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ↔ (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁)))) |
29 | 26, 28 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘𝑁) ∧ 𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))) → ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)))) |
30 | 29 | rexlimdva 3013 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → 𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)))) |
31 | 30 | abssdv 3639 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ⊆ (ℕ0
↑𝑚 (1...𝑁))) |
32 | 15 | elpw2 4755 |
. . . . . . . . . . . 12
⊢ ({𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ 𝒫 (ℕ0
↑𝑚 (1...𝑁)) ↔ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ⊆ (ℕ0
↑𝑚 (1...𝑁))) |
33 | 31, 32 | sylibr 223 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ 𝒫 (ℕ0
↑𝑚 (1...𝑁))) |
34 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → (𝑑 ∈ 𝒫 (ℕ0
↑𝑚 (1...𝑁)) ↔ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ 𝒫 (ℕ0
↑𝑚 (1...𝑁)))) |
35 | 33, 34 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → 𝑑 ∈ 𝒫 (ℕ0
↑𝑚 (1...𝑁)))) |
36 | 35 | rexlimdvw 3016 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → 𝑑 ∈ 𝒫 (ℕ0
↑𝑚 (1...𝑁)))) |
37 | 36 | rexlimiv 3009 |
. . . . . . . 8
⊢
(∃𝑘 ∈
(ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → 𝑑 ∈ 𝒫 (ℕ0
↑𝑚 (1...𝑁))) |
38 | 37 | abssi 3640 |
. . . . . . 7
⊢ {𝑑 ∣ ∃𝑘 ∈
(ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}} ⊆ 𝒫
(ℕ0 ↑𝑚 (1...𝑁)) |
39 | 18, 38 | eqsstri 3598 |
. . . . . 6
⊢ ran
(𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) ⊆ 𝒫
(ℕ0 ↑𝑚 (1...𝑁)) |
40 | 16, 39 | ssexi 4731 |
. . . . 5
⊢ ran
(𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) ∈ V |
41 | 14, 1, 40 | fvmpt 6191 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (Dioph‘𝑁) =
ran (𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
42 | 41 | eleq2d 2673 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐷 ∈
(Dioph‘𝑁) ↔
𝐷 ∈ ran (𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}))) |
43 | | ovex 6577 |
. . . . . 6
⊢
(ℕ0 ↑𝑚 (1...𝑘)) ∈ V |
44 | 43 | abrexex 7033 |
. . . . 5
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))𝑡 = (𝑢 ↾ (1...𝑁))} ∈ V |
45 | | simpl 472 |
. . . . . . 7
⊢ ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → 𝑡 = (𝑢 ↾ (1...𝑁))) |
46 | 45 | reximi 2994 |
. . . . . 6
⊢
(∃𝑢 ∈
(ℕ0 ↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))𝑡 = (𝑢 ↾ (1...𝑁))) |
47 | 46 | ss2abi 3637 |
. . . . 5
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ⊆ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))𝑡 = (𝑢 ↾ (1...𝑁))} |
48 | 44, 47 | ssexi 4731 |
. . . 4
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ V |
49 | 17, 48 | elrnmpt2 6671 |
. . 3
⊢ (𝐷 ∈ ran (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) ↔ ∃𝑘 ∈ (ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝐷 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) |
50 | 42, 49 | syl6bb 275 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐷 ∈
(Dioph‘𝑁) ↔
∃𝑘 ∈
(ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝐷 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
51 | 4, 50 | biadan2 672 |
1
⊢ (𝐷 ∈ (Dioph‘𝑁) ↔ (𝑁 ∈ ℕ0 ∧
∃𝑘 ∈
(ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝐷 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑𝑚 (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |