Step | Hyp | Ref
| Expression |
1 | | df-dioph 40309 |
. . . 4
⊢ Dioph =
(𝑛 ∈
ℕ0 ↦ ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)})) |
2 | 1 | dmmptss 6118 |
. . 3
⊢ dom Dioph
⊆ ℕ0 |
3 | | elfvdm 6767 |
. . 3
⊢ (𝐷 ∈ (Dioph‘𝑁) → 𝑁 ∈ dom Dioph) |
4 | 2, 3 | sseldi 3913 |
. 2
⊢ (𝐷 ∈ (Dioph‘𝑁) → 𝑁 ∈
ℕ0) |
5 | | fveq2 6735 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑁)) |
6 | | eqidd 2739 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (mzPoly‘(1...𝑘)) = (mzPoly‘(1...𝑘))) |
7 | | oveq2 7239 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁)) |
8 | 7 | reseq2d 5865 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → (𝑢 ↾ (1...𝑛)) = (𝑢 ↾ (1...𝑁))) |
9 | 8 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (𝑡 = (𝑢 ↾ (1...𝑛)) ↔ 𝑡 = (𝑢 ↾ (1...𝑁)))) |
10 | 9 | anbi1d 633 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0) ↔ (𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0))) |
11 | 10 | rexbidv 3224 |
. . . . . . . 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 7304 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}) = (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
14 | 13 | rneqd 5821 |
. . . . 5
⊢ (𝑛 = 𝑁 → ran (𝑘 ∈ (ℤ≥‘𝑛), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑛)) ∧ (𝑝‘𝑢) = 0)}) = ran (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
15 | | ovex 7264 |
. . . . . . 7
⊢
(ℕ0 ↑m (1...𝑁)) ∈ V |
16 | 15 | pwex 5287 |
. . . . . 6
⊢ 𝒫
(ℕ0 ↑m (1...𝑁)) ∈ V |
17 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) = (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) |
18 | 17 | rnmpo 7361 |
. . . . . . 7
⊢ ran
(𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) = {𝑑 ∣ ∃𝑘 ∈ (ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}} |
19 | | elmapi 8550 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (ℕ0
↑m (1...𝑘))
→ 𝑢:(1...𝑘)⟶ℕ0) |
20 | | fzss2 13176 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...𝑘)) |
21 | | fssres 6603 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢:(1...𝑘)⟶ℕ0 ∧ (1...𝑁) ⊆ (1...𝑘)) → (𝑢 ↾ (1...𝑁)):(1...𝑁)⟶ℕ0) |
22 | 19, 20, 21 | syl2anr 600 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈
(ℤ≥‘𝑁) ∧ 𝑢 ∈ (ℕ0
↑m (1...𝑘))) → (𝑢 ↾ (1...𝑁)):(1...𝑁)⟶ℕ0) |
23 | | nn0ex 12120 |
. . . . . . . . . . . . . . . . 17
⊢
ℕ0 ∈ V |
24 | | ovex 7264 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑁) ∈
V |
25 | 23, 24 | elmap 8572 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑m (1...𝑁))
↔ (𝑢 ↾
(1...𝑁)):(1...𝑁)⟶ℕ0) |
26 | 22, 25 | sylibr 237 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈
(ℤ≥‘𝑁) ∧ 𝑢 ∈ (ℕ0
↑m (1...𝑘))) → (𝑢 ↾ (1...𝑁)) ∈ (ℕ0
↑m (1...𝑁))) |
27 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝑢 ↾ (1...𝑁)) → (𝑡 ∈ (ℕ0
↑m (1...𝑁))
↔ (𝑢 ↾
(1...𝑁)) ∈
(ℕ0 ↑m (1...𝑁)))) |
28 | 27 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → (𝑡 ∈ (ℕ0
↑m (1...𝑁))
↔ (𝑢 ↾
(1...𝑁)) ∈
(ℕ0 ↑m (1...𝑁)))) |
29 | 26, 28 | syl5ibrcom 250 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘𝑁) ∧ 𝑢 ∈ (ℕ0
↑m (1...𝑘))) → ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → 𝑡 ∈ (ℕ0
↑m (1...𝑁)))) |
30 | 29 | rexlimdva 3211 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → 𝑡 ∈ (ℕ0
↑m (1...𝑁)))) |
31 | 30 | abssdv 3996 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ⊆ (ℕ0
↑m (1...𝑁))) |
32 | 15 | elpw2 5252 |
. . . . . . . . . . . 12
⊢ ({𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ 𝒫 (ℕ0
↑m (1...𝑁))
↔ {𝑡 ∣
∃𝑢 ∈
(ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ⊆ (ℕ0
↑m (1...𝑁))) |
33 | 31, 32 | sylibr 237 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ 𝒫 (ℕ0
↑m (1...𝑁))) |
34 | | eleq1 2826 |
. . . . . . . . . . 11
⊢ (𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → (𝑑 ∈ 𝒫 (ℕ0
↑m (1...𝑁))
↔ {𝑡 ∣
∃𝑢 ∈
(ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ 𝒫 (ℕ0
↑m (1...𝑁)))) |
35 | 33, 34 | syl5ibrcom 250 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → 𝑑 ∈ 𝒫 (ℕ0
↑m (1...𝑁)))) |
36 | 35 | rexlimdvw 3217 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑁) → (∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → 𝑑 ∈ 𝒫 (ℕ0
↑m (1...𝑁)))) |
37 | 36 | rexlimiv 3207 |
. . . . . . . 8
⊢
(∃𝑘 ∈
(ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} → 𝑑 ∈ 𝒫 (ℕ0
↑m (1...𝑁))) |
38 | 37 | abssi 3997 |
. . . . . . 7
⊢ {𝑑 ∣ ∃𝑘 ∈
(ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝑑 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}} ⊆ 𝒫
(ℕ0 ↑m (1...𝑁)) |
39 | 18, 38 | eqsstri 3949 |
. . . . . 6
⊢ ran
(𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) ⊆ 𝒫
(ℕ0 ↑m (1...𝑁)) |
40 | 16, 39 | ssexi 5229 |
. . . . 5
⊢ ran
(𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) ∈ V |
41 | 14, 1, 40 | fvmpt 6836 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (Dioph‘𝑁) =
ran (𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)})) |
42 | 41 | eleq2d 2824 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐷 ∈
(Dioph‘𝑁) ↔
𝐷 ∈ ran (𝑘 ∈
(ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}))) |
43 | | ovex 7264 |
. . . . . 6
⊢
(ℕ0 ↑m (1...𝑘)) ∈ V |
44 | 43 | abrexex 7753 |
. . . . 5
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))𝑡 = (𝑢 ↾ (1...𝑁))} ∈ V |
45 | | simpl 486 |
. . . . . . 7
⊢ ((𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → 𝑡 = (𝑢 ↾ (1...𝑁))) |
46 | 45 | reximi 3173 |
. . . . . 6
⊢
(∃𝑢 ∈
(ℕ0 ↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0) → ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))𝑡 = (𝑢 ↾ (1...𝑁))) |
47 | 46 | ss2abi 3994 |
. . . . 5
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ⊆ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))𝑡 = (𝑢 ↾ (1...𝑁))} |
48 | 44, 47 | ssexi 5229 |
. . . 4
⊢ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)} ∈ V |
49 | 17, 48 | elrnmpo 7364 |
. . 3
⊢ (𝐷 ∈ ran (𝑘 ∈ (ℤ≥‘𝑁), 𝑝 ∈ (mzPoly‘(1...𝑘)) ↦ {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) ↔ ∃𝑘 ∈ (ℤ≥‘𝑁)∃𝑝 ∈ (mzPoly‘(1...𝑘))𝐷 = {𝑡 ∣ ∃𝑢 ∈ (ℕ0
↑m (1...𝑘))(𝑡 = (𝑢 ↾ (1...𝑁)) ∧ (𝑝‘𝑢) = 0)}) |
50 | 42, 49 | bitrdi 290 |
. 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)})) |