Metamath Proof Explorer

Theorem diophrex

Description: Projecting a Diophantine set by removing a coordinate results in a Diophantine set. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion diophrex ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ 𝑆 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑎 = 𝑡 → ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑡 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
2 1 rexbidv ⊢ ( 𝑎 = 𝑡 → ( ∃ 𝑏 ∈ 𝑆 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ ∃ 𝑏 ∈ 𝑆 𝑡 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
3 reseq1 ⊢ ( 𝑏 = 𝑢 → ( 𝑏 ↾ ( 1 ... 𝑁 ) ) = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) )
4 3 eqeq2d ⊢ ( 𝑏 = 𝑢 → ( 𝑡 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ) )
5 4 cbvrexvw ⊢ ( ∃ 𝑏 ∈ 𝑆 𝑡 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ ∃ 𝑢 ∈ 𝑆 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) )
6 2 5 bitrdi ⊢ ( 𝑎 = 𝑡 → ( ∃ 𝑏 ∈ 𝑆 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ ∃ 𝑢 ∈ 𝑆 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ) )
7 6 cbvabv ⊢ { 𝑎 ∣ ∃ 𝑏 ∈ 𝑆 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } = { 𝑡 ∣ ∃ 𝑢 ∈ 𝑆 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) }
8 rexeq ⊢ ( 𝑆 = { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } → ( ∃ 𝑏 ∈ 𝑆 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ ∃ 𝑏 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
9 8 abbidv ⊢ ( 𝑆 = { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } → { 𝑎 ∣ ∃ 𝑏 ∈ 𝑆 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } = { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } )
10 9 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝑆 = { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } ) → { 𝑎 ∣ ∃ 𝑏 ∈ 𝑆 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } = { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } )
11 eqeq1 ⊢ ( 𝑑 = 𝑏 → ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↔ 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ) )
12 11 anbi1d ⊢ ( 𝑑 = 𝑏 → ( ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ↔ ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ) )
13 12 rexbidv ⊢ ( 𝑑 = 𝑏 → ( ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ↔ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ) )
14 13 rexab ⊢ ( ∃ 𝑏 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ ∃ 𝑏 ( ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
15 r19.41v ⊢ ( ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ( ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
16 15 exbii ⊢ ( ∃ 𝑏 ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ∃ 𝑏 ( ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
17 rexcom4 ⊢ ( ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ∃ 𝑏 ( ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ∃ 𝑏 ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) )
18 anass ⊢ ( ( ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( ( 𝑐 ‘ 𝑒 ) = 0 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) )
19 18 exbii ⊢ ( ∃ 𝑏 ( ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ∃ 𝑏 ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( ( 𝑐 ‘ 𝑒 ) = 0 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) )
20 vex ⊢ 𝑒 ∈ V
21 20 resex ⊢ ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∈ V
22 reseq1 ⊢ ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) → ( 𝑏 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) )
23 22 eqeq2d ⊢ ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) → ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ 𝑎 = ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) ) )
24 23 anbi2d ⊢ ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) → ( ( ( 𝑐 ‘ 𝑒 ) = 0 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ( ( 𝑐 ‘ 𝑒 ) = 0 ∧ 𝑎 = ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) ) ) )
25 21 24 ceqsexv ⊢ ( ∃ 𝑏 ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( ( 𝑐 ‘ 𝑒 ) = 0 ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ) ↔ ( ( 𝑐 ‘ 𝑒 ) = 0 ∧ 𝑎 = ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) ) )
26 19 25 bitri ⊢ ( ∃ 𝑏 ( ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ( ( 𝑐 ‘ 𝑒 ) = 0 ∧ 𝑎 = ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) ) )
27 ancom ⊢ ( ( ( 𝑐 ‘ 𝑒 ) = 0 ∧ 𝑎 = ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) ) ↔ ( 𝑎 = ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) )
28 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
29 fzss2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 ) )
30 resabs1 ⊢ ( ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 ) → ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
31 28 29 30 3syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) )
32 31 eqeq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → ( 𝑎 = ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) ↔ 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ) )
33 32 anbi1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → ( ( 𝑎 = ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ↔ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ) )
34 27 33 bitrid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → ( ( ( 𝑐 ‘ 𝑒 ) = 0 ∧ 𝑎 = ( ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ↾ ( 1 ... 𝑁 ) ) ) ↔ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ) )
35 26 34 bitrid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → ( ∃ 𝑏 ( ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ( 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ) )
36 35 rexbidv ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → ( ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ∃ 𝑏 ( ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ) )
37 17 36 bitr3id ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → ( ∃ 𝑏 ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ) )
38 16 37 bitr3id ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → ( ∃ 𝑏 ( ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ∧ 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ) ↔ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ) )
39 14 38 bitrid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → ( ∃ 𝑏 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) ↔ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) ) )
40 39 abbidv ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } = { 𝑎 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } )
41 eldioph3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → { 𝑎 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
42 41 3ad2antl1 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → { 𝑎 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑎 = ( 𝑒 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
43 40 42 eqeltrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } ∈ ( Dioph ‘ 𝑁 ) )
44 43 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝑆 = { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } ) → { 𝑎 ∣ ∃ 𝑏 ∈ { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } ∈ ( Dioph ‘ 𝑁 ) )
45 10 44 eqeltrd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) ∧ 𝑐 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝑆 = { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } ) → { 𝑎 ∣ ∃ 𝑏 ∈ 𝑆 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } ∈ ( Dioph ‘ 𝑁 ) )
46 eldioph3b ⊢ ( 𝑆 ∈ ( Dioph ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℕ0 ∧ ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝑆 = { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } ) )
47 46 simprbi ⊢ ( 𝑆 ∈ ( Dioph ‘ 𝑀 ) → ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝑆 = { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } )
48 47 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) → ∃ 𝑐 ∈ ( mzPoly ‘ ℕ ) 𝑆 = { 𝑑 ∣ ∃ 𝑒 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑒 ↾ ( 1 ... 𝑀 ) ) ∧ ( 𝑐 ‘ 𝑒 ) = 0 ) } )
49 45 48 r19.29a ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ 𝑆 𝑎 = ( 𝑏 ↾ ( 1 ... 𝑁 ) ) } ∈ ( Dioph ‘ 𝑁 ) )
50 7 49 eqeltrrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑆 ∈ ( Dioph ‘ 𝑀 ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ 𝑆 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) } ∈ ( Dioph ‘ 𝑁 ) )