Metamath Proof Explorer

Theorem eldioph4b

Description: Membership in Dioph expressed using a quantified union to add witness variables instead of a restriction to remove them. (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Hypotheses eldioph4b.a ⊢ 𝑊 ∈ V
eldioph4b.b ⊢ ¬ 𝑊 ∈ Fin
eldioph4b.c ⊢ ( 𝑊 ∩ ℕ ) = ∅
Assertion eldioph4b ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) 𝑆 = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } ) )

Proof

Step Hyp Ref Expression
1 eldioph4b.a ⊢ 𝑊 ∈ V
2 eldioph4b.b ⊢ ¬ 𝑊 ∈ Fin
3 eldioph4b.c ⊢ ( 𝑊 ∩ ℕ ) = ∅
4 eldiophelnn0 ⊢ ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) → 𝑁 ∈ ℕ0 )
5 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
6 1 5 unex ⊢ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ∈ V
7 6 jctr ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ∈ V ) )
8 2 intnanr ⊢ ¬ ( 𝑊 ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin )
9 unfir ⊢ ( ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ∈ Fin → ( 𝑊 ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ) )
10 8 9 mto ⊢ ¬ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ∈ Fin
11 ssun2 ⊢ ( 1 ... 𝑁 ) ⊆ ( 𝑊 ∪ ( 1 ... 𝑁 ) )
12 10 11 pm3.2i ⊢ ( ¬ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) )
13 eldioph2b ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ∈ V ) ∧ ( ¬ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ) → ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) 𝑆 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
14 7 12 13 sylancl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) 𝑆 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
15 elmapssres ⊢ ( ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ∧ ( 1 ... 𝑁 ) ⊆ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
16 11 15 mpan2 ⊢ ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
17 16 adantr ⊢ ( ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
18 ssun1 ⊢ 𝑊 ⊆ ( 𝑊 ∪ ( 1 ... 𝑁 ) )
19 elmapssres ⊢ ( ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ∧ 𝑊 ⊆ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → ( 𝑢 ↾ 𝑊 ) ∈ ( ℕ0 ↑m 𝑊 ) )
20 18 19 mpan2 ⊢ ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → ( 𝑢 ↾ 𝑊 ) ∈ ( ℕ0 ↑m 𝑊 ) )
21 20 adantr ⊢ ( ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → ( 𝑢 ↾ 𝑊 ) ∈ ( ℕ0 ↑m 𝑊 ) )
22 uncom ⊢ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑢 ↾ 𝑊 ) ) = ( ( 𝑢 ↾ 𝑊 ) ∪ ( 𝑢 ↾ ( 1 ... 𝑁 ) ) )
23 resundi ⊢ ( 𝑢 ↾ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) = ( ( 𝑢 ↾ 𝑊 ) ∪ ( 𝑢 ↾ ( 1 ... 𝑁 ) ) )
24 22 23 eqtr4i ⊢ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑢 ↾ 𝑊 ) ) = ( 𝑢 ↾ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) )
25 elmapi ⊢ ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → 𝑢 : ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ⟶ ℕ0 )
26 ffn ⊢ ( 𝑢 : ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ⟶ ℕ0 → 𝑢 Fn ( 𝑊 ∪ ( 1 ... 𝑁 ) ) )
27 fnresdm ⊢ ( 𝑢 Fn ( 𝑊 ∪ ( 1 ... 𝑁 ) ) → ( 𝑢 ↾ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) = 𝑢 )
28 25 26 27 3syl ⊢ ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → ( 𝑢 ↾ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) = 𝑢 )
29 24 28 syl5eq ⊢ ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑢 ↾ 𝑊 ) ) = 𝑢 )
30 29 fveqeq2d ⊢ ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → ( ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑢 ↾ 𝑊 ) ) ) = 0 ↔ ( 𝑝 ‘ 𝑢 ) = 0 ) )
31 30 biimpar ⊢ ( ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑢 ↾ 𝑊 ) ) ) = 0 )
32 uneq2 ⊢ ( 𝑤 = ( 𝑢 ↾ 𝑊 ) → ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ 𝑤 ) = ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑢 ↾ 𝑊 ) ) )
33 32 fveqeq2d ⊢ ( 𝑤 = ( 𝑢 ↾ 𝑊 ) → ( ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ 𝑤 ) ) = 0 ↔ ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑢 ↾ 𝑊 ) ) ) = 0 ) )
34 33 rspcev ⊢ ( ( ( 𝑢 ↾ 𝑊 ) ∈ ( ℕ0 ↑m 𝑊 ) ∧ ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ ( 𝑢 ↾ 𝑊 ) ) ) = 0 ) → ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ 𝑤 ) ) = 0 )
35 21 31 34 syl2anc ⊢ ( ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ 𝑤 ) ) = 0 )
36 17 35 jca ⊢ ( ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ 𝑤 ) ) = 0 ) )
37 eleq1 ⊢ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) → ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ↔ ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) )
38 uneq1 ⊢ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) → ( 𝑡 ∪ 𝑤 ) = ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ 𝑤 ) )
39 38 fveqeq2d ⊢ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ↔ ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ 𝑤 ) ) = 0 ) )
40 39 rexbidv ⊢ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) → ( ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ↔ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ 𝑤 ) ) = 0 ) )
41 37 40 anbi12d ⊢ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) → ( ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) ↔ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∪ 𝑤 ) ) = 0 ) ) )
42 36 41 syl5ibrcom ⊢ ( ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) → ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) ) )
43 42 expimpd ⊢ ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝑝 ‘ 𝑢 ) = 0 ∧ 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) ) )
44 43 ancomsd ⊢ ( 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → ( ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) ) )
45 44 rexlimiv ⊢ ( ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) → ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) )
46 uncom ⊢ ( 𝑡 ∪ 𝑤 ) = ( 𝑤 ∪ 𝑡 )
47 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
48 sslin ⊢ ( ( 1 ... 𝑁 ) ⊆ ℕ → ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ⊆ ( 𝑊 ∩ ℕ ) )
49 47 48 ax-mp ⊢ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ⊆ ( 𝑊 ∩ ℕ )
50 49 3 sseqtri ⊢ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ⊆ ∅
51 ss0 ⊢ ( ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ⊆ ∅ → ( 𝑊 ∩ ( 1 ... 𝑁 ) ) = ∅ )
52 50 51 ax-mp ⊢ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) = ∅
53 52 reseq2i ⊢ ( 𝑤 ↾ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ) = ( 𝑤 ↾ ∅ )
54 res0 ⊢ ( 𝑤 ↾ ∅ ) = ∅
55 53 54 eqtri ⊢ ( 𝑤 ↾ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ) = ∅
56 52 reseq2i ⊢ ( 𝑡 ↾ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ) = ( 𝑡 ↾ ∅ )
57 res0 ⊢ ( 𝑡 ↾ ∅ ) = ∅
58 56 57 eqtri ⊢ ( 𝑡 ↾ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ) = ∅
59 55 58 eqtr4i ⊢ ( 𝑤 ↾ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ) = ( 𝑡 ↾ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) )
60 elmapresaun ⊢ ( ( 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ( 𝑤 ↾ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ) = ( 𝑡 ↾ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ) ) → ( 𝑤 ∪ 𝑡 ) ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) )
61 59 60 mp3an3 ⊢ ( ( 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( 𝑤 ∪ 𝑡 ) ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) )
62 61 ancoms ⊢ ( ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ) → ( 𝑤 ∪ 𝑡 ) ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) )
63 46 62 eqeltrid ⊢ ( ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ) → ( 𝑡 ∪ 𝑤 ) ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) )
64 63 adantr ⊢ ( ( ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ) ∧ ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) → ( 𝑡 ∪ 𝑤 ) ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) )
65 46 reseq1i ⊢ ( ( 𝑡 ∪ 𝑤 ) ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑤 ∪ 𝑡 ) ↾ ( 1 ... 𝑁 ) )
66 elmapresaunres2 ⊢ ( ( 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ( 𝑤 ↾ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ) = ( 𝑡 ↾ ( 𝑊 ∩ ( 1 ... 𝑁 ) ) ) ) → ( ( 𝑤 ∪ 𝑡 ) ↾ ( 1 ... 𝑁 ) ) = 𝑡 )
67 59 66 mp3an3 ⊢ ( ( 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ∧ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ) → ( ( 𝑤 ∪ 𝑡 ) ↾ ( 1 ... 𝑁 ) ) = 𝑡 )
68 67 ancoms ⊢ ( ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ) → ( ( 𝑤 ∪ 𝑡 ) ↾ ( 1 ... 𝑁 ) ) = 𝑡 )
69 65 68 eqtr2id ⊢ ( ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ) → 𝑡 = ( ( 𝑡 ∪ 𝑤 ) ↾ ( 1 ... 𝑁 ) ) )
70 69 adantr ⊢ ( ( ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ) ∧ ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) → 𝑡 = ( ( 𝑡 ∪ 𝑤 ) ↾ ( 1 ... 𝑁 ) ) )
71 simpr ⊢ ( ( ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ) ∧ ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) → ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 )
72 reseq1 ⊢ ( 𝑢 = ( 𝑡 ∪ 𝑤 ) → ( 𝑢 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑡 ∪ 𝑤 ) ↾ ( 1 ... 𝑁 ) ) )
73 72 eqeq2d ⊢ ( 𝑢 = ( 𝑡 ∪ 𝑤 ) → ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑡 = ( ( 𝑡 ∪ 𝑤 ) ↾ ( 1 ... 𝑁 ) ) ) )
74 fveqeq2 ⊢ ( 𝑢 = ( 𝑡 ∪ 𝑤 ) → ( ( 𝑝 ‘ 𝑢 ) = 0 ↔ ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) )
75 73 74 anbi12d ⊢ ( 𝑢 = ( 𝑡 ∪ 𝑤 ) → ( ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ↔ ( 𝑡 = ( ( 𝑡 ∪ 𝑤 ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) ) )
76 75 rspcev ⊢ ( ( ( 𝑡 ∪ 𝑤 ) ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ∧ ( 𝑡 = ( ( 𝑡 ∪ 𝑤 ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) ) → ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) )
77 64 70 71 76 syl12anc ⊢ ( ( ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ) ∧ ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) → ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) )
78 77 r19.29an ⊢ ( ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) → ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) )
79 45 78 impbii ⊢ ( ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ↔ ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) )
80 79 abbii ⊢ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) }
81 df-rab ⊢ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } = { 𝑡 ∣ ( 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∧ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ) }
82 80 81 eqtr4i ⊢ { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 }
83 82 eqeq2i ⊢ ( 𝑆 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ↔ 𝑆 = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } )
84 83 rexbii ⊢ ( ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) 𝑆 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ↔ ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) 𝑆 = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } )
85 14 84 bitrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) 𝑆 = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } ) )
86 4 85 biadanii ⊢ ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) 𝑆 = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } ) )