Metamath Proof Explorer

Theorem diophren

Description: Change variables in a Diophantine set, using class notation. This allows already proved Diophantine sets to be reused in contexts with more variables. (Contributed by Stefan O'Rear, 16-Oct-2014) (Revised by Stefan O'Rear, 5-Jun-2015)

Ref Expression
Assertion diophren ( ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ 𝑆 } ∈ ( Dioph ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 zex ⊢ ℤ ∈ V
2 difexg ⊢ ( ℤ ∈ V → ( ℤ ∖ ℕ ) ∈ V )
3 1 2 ax-mp ⊢ ( ℤ ∖ ℕ ) ∈ V
4 ominf ⊢ ¬ ω ∈ Fin
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 0p1e1 ⊢ ( 0 + 1 ) = 1
7 6 fveq2i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ( ℤ≥ ‘ 1 )
8 5 7 eqtr4i ⊢ ℕ = ( ℤ≥ ‘ ( 0 + 1 ) )
9 8 difeq2i ⊢ ( ℤ ∖ ℕ ) = ( ℤ ∖ ( ℤ≥ ‘ ( 0 + 1 ) ) )
10 0z ⊢ 0 ∈ ℤ
11 lzenom ⊢ ( 0 ∈ ℤ → ( ℤ ∖ ( ℤ≥ ‘ ( 0 + 1 ) ) ) ≈ ω )
12 10 11 ax-mp ⊢ ( ℤ ∖ ( ℤ≥ ‘ ( 0 + 1 ) ) ) ≈ ω
13 9 12 eqbrtri ⊢ ( ℤ ∖ ℕ ) ≈ ω
14 enfi ⊢ ( ( ℤ ∖ ℕ ) ≈ ω → ( ( ℤ ∖ ℕ ) ∈ Fin ↔ ω ∈ Fin ) )
15 13 14 ax-mp ⊢ ( ( ℤ ∖ ℕ ) ∈ Fin ↔ ω ∈ Fin )
16 4 15 mtbir ⊢ ¬ ( ℤ ∖ ℕ ) ∈ Fin
17 incom ⊢ ( ( ℤ ∖ ℕ ) ∩ ℕ ) = ( ℕ ∩ ( ℤ ∖ ℕ ) )
18 disjdif ⊢ ( ℕ ∩ ( ℤ ∖ ℕ ) ) = ∅
19 17 18 eqtri ⊢ ( ( ℤ ∖ ℕ ) ∩ ℕ ) = ∅
20 3 16 19 eldioph4b ⊢ ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) 𝑆 = { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } ) )
21 simpr ⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) → 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) )
22 simp-4r ⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) → 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) )
23 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
24 23 mapco2 ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) → ( 𝑎 ∘ 𝐹 ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
25 21 22 24 syl2anc ⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) → ( 𝑎 ∘ 𝐹 ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) )
26 uneq1 ⊢ ( 𝑐 = ( 𝑎 ∘ 𝐹 ) → ( 𝑐 ∪ 𝑑 ) = ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) )
27 26 fveqeq2d ⊢ ( 𝑐 = ( 𝑎 ∘ 𝐹 ) → ( ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 ↔ ( 𝑏 ‘ ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) ) = 0 ) )
28 27 rexbidv ⊢ ( 𝑐 = ( 𝑎 ∘ 𝐹 ) → ( ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 ↔ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) ) = 0 ) )
29 28 elrab3 ⊢ ( ( 𝑎 ∘ 𝐹 ) ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) → ( ( 𝑎 ∘ 𝐹 ) ∈ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } ↔ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) ) = 0 ) )
30 25 29 syl ⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) → ( ( 𝑎 ∘ 𝐹 ) ∈ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } ↔ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) ) = 0 ) )
31 simp-5r ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) )
32 simplr ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) )
33 simpr ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) )
34 coundi ⊢ ( ( 𝑎 ∪ 𝑑 ) ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) = ( ( ( 𝑎 ∪ 𝑑 ) ∘ 𝐹 ) ∪ ( ( 𝑎 ∪ 𝑑 ) ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) )
35 coundir ⊢ ( ( 𝑎 ∪ 𝑑 ) ∘ 𝐹 ) = ( ( 𝑎 ∘ 𝐹 ) ∪ ( 𝑑 ∘ 𝐹 ) )
36 elmapi ⊢ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) → 𝑑 : ( ℤ ∖ ℕ ) ⟶ ℕ0 )
37 36 3ad2ant3 ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → 𝑑 : ( ℤ ∖ ℕ ) ⟶ ℕ0 )
38 simp1 ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) )
39 incom ⊢ ( ( ℤ ∖ ℕ ) ∩ ( 1 ... 𝑀 ) ) = ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) )
40 fz1ssnn ⊢ ( 1 ... 𝑀 ) ⊆ ℕ
41 ssdisj ⊢ ( ( ( 1 ... 𝑀 ) ⊆ ℕ ∧ ( ℕ ∩ ( ℤ ∖ ℕ ) ) = ∅ ) → ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) = ∅ )
42 40 18 41 mp2an ⊢ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) = ∅
43 39 42 eqtri ⊢ ( ( ℤ ∖ ℕ ) ∩ ( 1 ... 𝑀 ) ) = ∅
44 43 a1i ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( ℤ ∖ ℕ ) ∩ ( 1 ... 𝑀 ) ) = ∅ )
45 coeq0i ⊢ ( ( 𝑑 : ( ℤ ∖ ℕ ) ⟶ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ ( ( ℤ ∖ ℕ ) ∩ ( 1 ... 𝑀 ) ) = ∅ ) → ( 𝑑 ∘ 𝐹 ) = ∅ )
46 37 38 44 45 syl3anc ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( 𝑑 ∘ 𝐹 ) = ∅ )
47 46 uneq2d ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( 𝑎 ∘ 𝐹 ) ∪ ( 𝑑 ∘ 𝐹 ) ) = ( ( 𝑎 ∘ 𝐹 ) ∪ ∅ ) )
48 35 47 syl5eq ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( 𝑎 ∪ 𝑑 ) ∘ 𝐹 ) = ( ( 𝑎 ∘ 𝐹 ) ∪ ∅ ) )
49 un0 ⊢ ( ( 𝑎 ∘ 𝐹 ) ∪ ∅ ) = ( 𝑎 ∘ 𝐹 )
50 48 49 eqtrdi ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( 𝑎 ∪ 𝑑 ) ∘ 𝐹 ) = ( 𝑎 ∘ 𝐹 ) )
51 coundir ⊢ ( ( 𝑎 ∪ 𝑑 ) ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) = ( ( 𝑎 ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) ∪ ( 𝑑 ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) )
52 elmapi ⊢ ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) → 𝑎 : ( 1 ... 𝑀 ) ⟶ ℕ0 )
53 52 3ad2ant2 ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → 𝑎 : ( 1 ... 𝑀 ) ⟶ ℕ0 )
54 f1oi ⊢ ( I ↾ ( ℤ ∖ ℕ ) ) : ( ℤ ∖ ℕ ) –1-1-onto→ ( ℤ ∖ ℕ )
55 f1of ⊢ ( ( I ↾ ( ℤ ∖ ℕ ) ) : ( ℤ ∖ ℕ ) –1-1-onto→ ( ℤ ∖ ℕ ) → ( I ↾ ( ℤ ∖ ℕ ) ) : ( ℤ ∖ ℕ ) ⟶ ( ℤ ∖ ℕ ) )
56 54 55 ax-mp ⊢ ( I ↾ ( ℤ ∖ ℕ ) ) : ( ℤ ∖ ℕ ) ⟶ ( ℤ ∖ ℕ )
57 coeq0i ⊢ ( ( 𝑎 : ( 1 ... 𝑀 ) ⟶ ℕ0 ∧ ( I ↾ ( ℤ ∖ ℕ ) ) : ( ℤ ∖ ℕ ) ⟶ ( ℤ ∖ ℕ ) ∧ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) = ∅ ) → ( 𝑎 ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) = ∅ )
58 56 42 57 mp3an23 ⊢ ( 𝑎 : ( 1 ... 𝑀 ) ⟶ ℕ0 → ( 𝑎 ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) = ∅ )
59 53 58 syl ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( 𝑎 ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) = ∅ )
60 coires1 ⊢ ( 𝑑 ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) = ( 𝑑 ↾ ( ℤ ∖ ℕ ) )
61 ffn ⊢ ( 𝑑 : ( ℤ ∖ ℕ ) ⟶ ℕ0 → 𝑑 Fn ( ℤ ∖ ℕ ) )
62 fnresdm ⊢ ( 𝑑 Fn ( ℤ ∖ ℕ ) → ( 𝑑 ↾ ( ℤ ∖ ℕ ) ) = 𝑑 )
63 36 61 62 3syl ⊢ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) → ( 𝑑 ↾ ( ℤ ∖ ℕ ) ) = 𝑑 )
64 60 63 syl5eq ⊢ ( 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) → ( 𝑑 ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) = 𝑑 )
65 64 3ad2ant3 ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( 𝑑 ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) = 𝑑 )
66 59 65 uneq12d ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( 𝑎 ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) ∪ ( 𝑑 ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) = ( ∅ ∪ 𝑑 ) )
67 51 66 syl5eq ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( 𝑎 ∪ 𝑑 ) ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) = ( ∅ ∪ 𝑑 ) )
68 uncom ⊢ ( ∅ ∪ 𝑑 ) = ( 𝑑 ∪ ∅ )
69 un0 ⊢ ( 𝑑 ∪ ∅ ) = 𝑑
70 68 69 eqtri ⊢ ( ∅ ∪ 𝑑 ) = 𝑑
71 67 70 eqtrdi ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( 𝑎 ∪ 𝑑 ) ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) = 𝑑 )
72 50 71 uneq12d ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( ( 𝑎 ∪ 𝑑 ) ∘ 𝐹 ) ∪ ( ( 𝑎 ∪ 𝑑 ) ∘ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) = ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) )
73 34 72 syl5req ⊢ ( ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) = ( ( 𝑎 ∪ 𝑑 ) ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) )
74 31 32 33 73 syl3anc ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) = ( ( 𝑎 ∪ 𝑑 ) ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) )
75 74 fveq2d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( 𝑏 ‘ ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) ) = ( 𝑏 ‘ ( ( 𝑎 ∪ 𝑑 ) ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) )
76 nn0ssz ⊢ ℕ0 ⊆ ℤ
77 mapss ⊢ ( ( ℤ ∈ V ∧ ℕ0 ⊆ ℤ ) → ( ℕ0 ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ⊆ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) )
78 1 76 77 mp2an ⊢ ( ℕ0 ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ⊆ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) )
79 42 reseq2i ⊢ ( 𝑎 ↾ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) ) = ( 𝑎 ↾ ∅ )
80 res0 ⊢ ( 𝑎 ↾ ∅ ) = ∅
81 79 80 eqtri ⊢ ( 𝑎 ↾ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) ) = ∅
82 42 reseq2i ⊢ ( 𝑑 ↾ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) ) = ( 𝑑 ↾ ∅ )
83 res0 ⊢ ( 𝑑 ↾ ∅ ) = ∅
84 82 83 eqtri ⊢ ( 𝑑 ↾ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) ) = ∅
85 81 84 eqtr4i ⊢ ( 𝑎 ↾ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) ) = ( 𝑑 ↾ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) )
86 elmapresaun ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ∧ ( 𝑎 ↾ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) ) = ( 𝑑 ↾ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) ) ) → ( 𝑎 ∪ 𝑑 ) ∈ ( ℕ0 ↑m ( ( 1 ... 𝑀 ) ∪ ( ℤ ∖ ℕ ) ) ) )
87 uncom ⊢ ( ( 1 ... 𝑀 ) ∪ ( ℤ ∖ ℕ ) ) = ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) )
88 87 oveq2i ⊢ ( ℕ0 ↑m ( ( 1 ... 𝑀 ) ∪ ( ℤ ∖ ℕ ) ) ) = ( ℕ0 ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) )
89 86 88 eleqtrdi ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ∧ ( 𝑎 ↾ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) ) = ( 𝑑 ↾ ( ( 1 ... 𝑀 ) ∩ ( ℤ ∖ ℕ ) ) ) ) → ( 𝑎 ∪ 𝑑 ) ∈ ( ℕ0 ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) )
90 85 89 mp3an3 ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( 𝑎 ∪ 𝑑 ) ∈ ( ℕ0 ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) )
91 78 90 sseldi ⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( 𝑎 ∪ 𝑑 ) ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) )
92 91 adantll ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( 𝑎 ∪ 𝑑 ) ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) )
93 coeq1 ⊢ ( 𝑒 = ( 𝑎 ∪ 𝑑 ) → ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) = ( ( 𝑎 ∪ 𝑑 ) ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) )
94 93 fveq2d ⊢ ( 𝑒 = ( 𝑎 ∪ 𝑑 ) → ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) = ( 𝑏 ‘ ( ( 𝑎 ∪ 𝑑 ) ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) )
95 eqid ⊢ ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) = ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) )
96 fvex ⊢ ( 𝑏 ‘ ( ( 𝑎 ∪ 𝑑 ) ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ∈ V
97 94 95 96 fvmpt ⊢ ( ( 𝑎 ∪ 𝑑 ) ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) → ( ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ‘ ( 𝑎 ∪ 𝑑 ) ) = ( 𝑏 ‘ ( ( 𝑎 ∪ 𝑑 ) ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) )
98 92 97 syl ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ‘ ( 𝑎 ∪ 𝑑 ) ) = ( 𝑏 ‘ ( ( 𝑎 ∪ 𝑑 ) ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) )
99 75 98 eqtr4d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( 𝑏 ‘ ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) ) = ( ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ‘ ( 𝑎 ∪ 𝑑 ) ) )
100 99 eqeq1d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) ∧ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ) → ( ( 𝑏 ‘ ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) ) = 0 ↔ ( ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ‘ ( 𝑎 ∪ 𝑑 ) ) = 0 ) )
101 100 rexbidva ⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) → ( ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( ( 𝑎 ∘ 𝐹 ) ∪ 𝑑 ) ) = 0 ↔ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ‘ ( 𝑎 ∪ 𝑑 ) ) = 0 ) )
102 30 101 bitrd ⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ) → ( ( 𝑎 ∘ 𝐹 ) ∈ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } ↔ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ‘ ( 𝑎 ∪ 𝑑 ) ) = 0 ) )
103 102 rabbidva ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ‘ ( 𝑎 ∪ 𝑑 ) ) = 0 } )
104 simplll ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) → 𝑀 ∈ ℕ0 )
105 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
106 3 105 unex ⊢ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ∈ V
107 106 a1i ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) → ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ∈ V )
108 simpr ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) → 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) )
109 56 a1i ⊢ ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) → ( I ↾ ( ℤ ∖ ℕ ) ) : ( ℤ ∖ ℕ ) ⟶ ( ℤ ∖ ℕ ) )
110 id ⊢ ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) → 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) )
111 incom ⊢ ( ( ℤ ∖ ℕ ) ∩ ( 1 ... 𝑁 ) ) = ( ( 1 ... 𝑁 ) ∩ ( ℤ ∖ ℕ ) )
112 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
113 ssdisj ⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( ℕ ∩ ( ℤ ∖ ℕ ) ) = ∅ ) → ( ( 1 ... 𝑁 ) ∩ ( ℤ ∖ ℕ ) ) = ∅ )
114 112 18 113 mp2an ⊢ ( ( 1 ... 𝑁 ) ∩ ( ℤ ∖ ℕ ) ) = ∅
115 111 114 eqtri ⊢ ( ( ℤ ∖ ℕ ) ∩ ( 1 ... 𝑁 ) ) = ∅
116 115 a1i ⊢ ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) → ( ( ℤ ∖ ℕ ) ∩ ( 1 ... 𝑁 ) ) = ∅ )
117 fun ⊢ ( ( ( ( I ↾ ( ℤ ∖ ℕ ) ) : ( ℤ ∖ ℕ ) ⟶ ( ℤ ∖ ℕ ) ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ ( ( ℤ ∖ ℕ ) ∩ ( 1 ... 𝑁 ) ) = ∅ ) → ( ( I ↾ ( ℤ ∖ ℕ ) ) ∪ 𝐹 ) : ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ⟶ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) )
118 109 110 116 117 syl21anc ⊢ ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) → ( ( I ↾ ( ℤ ∖ ℕ ) ) ∪ 𝐹 ) : ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ⟶ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) )
119 uncom ⊢ ( ( I ↾ ( ℤ ∖ ℕ ) ) ∪ 𝐹 ) = ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) )
120 119 feq1i ⊢ ( ( ( I ↾ ( ℤ ∖ ℕ ) ) ∪ 𝐹 ) : ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ⟶ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ↔ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) : ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ⟶ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) )
121 118 120 sylib ⊢ ( 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) → ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) : ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ⟶ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) )
122 121 ad3antlr ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) → ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) : ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ⟶ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) )
123 mzprename ⊢ ( ( ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ∈ V ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ∧ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) : ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ⟶ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) → ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) )
124 107 108 122 123 syl3anc ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) → ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) )
125 3 16 19 eldioph4i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ‘ ( 𝑎 ∪ 𝑑 ) ) = 0 } ∈ ( Dioph ‘ 𝑀 ) )
126 104 124 125 syl2anc ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( ( 𝑒 ∈ ( ℤ ↑m ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑀 ) ) ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ ( 𝐹 ∪ ( I ↾ ( ℤ ∖ ℕ ) ) ) ) ) ) ‘ ( 𝑎 ∪ 𝑑 ) ) = 0 } ∈ ( Dioph ‘ 𝑀 ) )
127 103 126 eqeltrd ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } } ∈ ( Dioph ‘ 𝑀 ) )
128 eleq2 ⊢ ( 𝑆 = { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } → ( ( 𝑎 ∘ 𝐹 ) ∈ 𝑆 ↔ ( 𝑎 ∘ 𝐹 ) ∈ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } ) )
129 128 rabbidv ⊢ ( 𝑆 = { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ 𝑆 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } } )
130 129 eleq1d ⊢ ( 𝑆 = { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } → ( { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ 𝑆 } ∈ ( Dioph ‘ 𝑀 ) ↔ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } } ∈ ( Dioph ‘ 𝑀 ) ) )
131 127 130 syl5ibrcom ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) ) → ( 𝑆 = { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ 𝑆 } ∈ ( Dioph ‘ 𝑀 ) ) )
132 131 rexlimdva ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ∃ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) 𝑆 = { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ 𝑆 } ∈ ( Dioph ‘ 𝑀 ) ) )
133 132 expimpd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑏 ∈ ( mzPoly ‘ ( ( ℤ ∖ ℕ ) ∪ ( 1 ... 𝑁 ) ) ) 𝑆 = { 𝑐 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( ℤ ∖ ℕ ) ) ( 𝑏 ‘ ( 𝑐 ∪ 𝑑 ) ) = 0 } ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ 𝑆 } ∈ ( Dioph ‘ 𝑀 ) ) )
134 20 133 syl5bi ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) → ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ 𝑆 } ∈ ( Dioph ‘ 𝑀 ) ) )
135 134 impcom ⊢ ( ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ 𝑆 } ∈ ( Dioph ‘ 𝑀 ) )
136 135 3impb ⊢ ( ( 𝑆 ∈ ( Dioph ‘ 𝑁 ) ∧ 𝑀 ∈ ℕ0 ∧ 𝐹 : ( 1 ... 𝑁 ) ⟶ ( 1 ... 𝑀 ) ) → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑀 ) ) ∣ ( 𝑎 ∘ 𝐹 ) ∈ 𝑆 } ∈ ( Dioph ‘ 𝑀 ) )