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