Theorem eldioph2b

Description: While Diophantine sets were defined to have a finite number of witness variables consequtively following the observable variables, this is not necessary; they can equivalently be taken to use any witness set ( S \ ( 1 ... N ) ) . For instance, in diophin we use this to take the two input sets to have disjoint witness sets. (Contributed by Stefan O'Rear, 8-Oct-2014)

	Ref	Expression
Assertion	eldioph2b	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) → ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		eldiophb	⊢ ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) 𝐴 = { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } ) )
2		simp-5r	⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) ∧ 𝑐 ∈ V ) ∧ ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑆 ∈ V )
3		simprr	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) → 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) )
4	3	ad2antrr	⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) ∧ 𝑐 ∈ V ) ∧ ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) )
5		simprl	⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) ∧ 𝑐 ∈ V ) ∧ ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 )
6		f1f	⊢ ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 → 𝑐 : ( 1 ... 𝑎 ) ⟶ 𝑆 )
7	5 6	syl	⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) ∧ 𝑐 ∈ V ) ∧ ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → 𝑐 : ( 1 ... 𝑎 ) ⟶ 𝑆 )
8		mzprename	⊢ ( ( 𝑆 ∈ V ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ∧ 𝑐 : ( 1 ... 𝑎 ) ⟶ 𝑆 ) → ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ∈ ( mzPoly ‘ 𝑆 ) )
9	2 4 7 8	syl3anc	⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) ∧ 𝑐 ∈ V ) ∧ ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ∈ ( mzPoly ‘ 𝑆 ) )
10		simprr	⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) ∧ 𝑐 ∈ V ) ∧ ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) )
11		diophrw	⊢ ( ( 𝑆 ∈ V ∧ 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } )
12	11	eqcomd	⊢ ( ( 𝑆 ∈ V ∧ 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) → { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ‘ 𝑢 ) = 0 ) } )
13	2 5 10 12	syl3anc	⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) ∧ 𝑐 ∈ V ) ∧ ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ‘ 𝑢 ) = 0 ) } )
14		fveq1	⊢ ( 𝑝 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) → ( 𝑝 ‘ 𝑢 ) = ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ‘ 𝑢 ) )
15	14	eqeq1d	⊢ ( 𝑝 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) → ( ( 𝑝 ‘ 𝑢 ) = 0 ↔ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ‘ 𝑢 ) = 0 ) )
16	15	anbi2d	⊢ ( 𝑝 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) → ( ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ↔ ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ‘ 𝑢 ) = 0 ) ) )
17	16	rexbidv	⊢ ( 𝑝 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) → ( ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) ↔ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ‘ 𝑢 ) = 0 ) ) )
18	17	abbidv	⊢ ( 𝑝 = ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ‘ 𝑢 ) = 0 ) } )
19	18	rspceeqv	⊢ ( ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ∈ ( mzPoly ‘ 𝑆 ) ∧ { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( ( 𝑒 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑏 ‘ ( 𝑒 ∘ 𝑐 ) ) ) ‘ 𝑢 ) = 0 ) } ) → ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
20	9 13 19	syl2anc	⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) ∧ 𝑐 ∈ V ) ∧ ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
21		simplll	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) → 𝑁 ∈ ℕ0 )
22		simplrl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) → ¬ 𝑆 ∈ Fin )
23		simplrr	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) → ( 1 ... 𝑁 ) ⊆ 𝑆 )
24		simprl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) → 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) )
25		eldioph2lem2	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆 ∧ 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) → ∃ 𝑐 ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
26	21 22 23 24 25	syl22anc	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) → ∃ 𝑐 ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
27		rexv	⊢ ( ∃ 𝑐 ∈ V ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ↔ ∃ 𝑐 ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
28	26 27	sylibr	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) → ∃ 𝑐 ∈ V ( 𝑐 : ( 1 ... 𝑎 ) –1-1→ 𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
29	20 28	r19.29a	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) → ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
30		eqeq1	⊢ ( 𝐴 = { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } → ( 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ↔ { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
31	30	rexbidv	⊢ ( 𝐴 = { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } → ( ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ↔ ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
32	29 31	syl5ibrcom	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ ( 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) ) ) → ( 𝐴 = { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } → ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
33	32	rexlimdvva	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) → ( ∃ 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) 𝐴 = { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } → ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
34	33	adantld	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑎 ∈ ( ℤ≥ ‘ 𝑁 ) ∃ 𝑏 ∈ ( mzPoly ‘ ( 1 ... 𝑎 ) ) 𝐴 = { 𝑡 ∣ ∃ 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝑎 ) ) ( 𝑡 = ( 𝑑 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑏 ‘ 𝑑 ) = 0 ) } ) → ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
35	1 34	biimtrid	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) → ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) → ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )
36		simpr	⊢ ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) ) ∧ 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) → 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } )
37		simplll	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) ) → 𝑁 ∈ ℕ0 )
38		simpllr	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) ) → 𝑆 ∈ V )
39		simplrr	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) ) → ( 1 ... 𝑁 ) ⊆ 𝑆 )
40		simpr	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) ) → 𝑝 ∈ ( mzPoly ‘ 𝑆 ) )
41		eldioph2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑆 ∈ V ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ∧ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
42	37 38 39 40 41	syl121anc	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
43	42	adantr	⊢ ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) ) ∧ 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) → { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ∈ ( Dioph ‘ 𝑁 ) )
44	36 43	eqeltrd	⊢ ( ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) ∧ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) ) ∧ 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) → 𝐴 ∈ ( Dioph ‘ 𝑁 ) )
45	44	rexlimdva2	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) → ( ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } → 𝐴 ∈ ( Dioph ‘ 𝑁 ) ) )
46	35 45	impbid	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑆 ∈ V ) ∧ ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝑆 ) ) → ( 𝐴 ∈ ( Dioph ‘ 𝑁 ) ↔ ∃ 𝑝 ∈ ( mzPoly ‘ 𝑆 ) 𝐴 = { 𝑡 ∣ ∃ 𝑢 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑡 = ( 𝑢 ↾ ( 1 ... 𝑁 ) ) ∧ ( 𝑝 ‘ 𝑢 ) = 0 ) } ) )