Theorem eldioph4i

Description: Forward-only version of eldioph4b . (Contributed by Stefan O'Rear, 16-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		eldioph4b.a	⊢ 𝑊 ∈ V
2		eldioph4b.b	⊢ ¬ 𝑊 ∈ Fin
3		eldioph4b.c	⊢ ( 𝑊 ∩ ℕ ) = ∅
4		uneq1	⊢ ( 𝑡 = 𝑎 → ( 𝑡 ∪ 𝑤 ) = ( 𝑎 ∪ 𝑤 ) )
5	4	fveqeq2d	⊢ ( 𝑡 = 𝑎 → ( ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ↔ ( 𝑃 ‘ ( 𝑎 ∪ 𝑤 ) ) = 0 ) )
6	5	rexbidv	⊢ ( 𝑡 = 𝑎 → ( ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ↔ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑎 ∪ 𝑤 ) ) = 0 ) )
7		uneq2	⊢ ( 𝑤 = 𝑏 → ( 𝑎 ∪ 𝑤 ) = ( 𝑎 ∪ 𝑏 ) )
8	7	fveqeq2d	⊢ ( 𝑤 = 𝑏 → ( ( 𝑃 ‘ ( 𝑎 ∪ 𝑤 ) ) = 0 ↔ ( 𝑃 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 ) )
9	8	cbvrexvw	⊢ ( ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑎 ∪ 𝑤 ) ) = 0 ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 )
10	6 9	bitrdi	⊢ ( 𝑡 = 𝑎 → ( ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 ) )
11	10	cbvrabv	⊢ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 }
12		fveq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ ( 𝑎 ∪ 𝑏 ) ) = ( 𝑃 ‘ ( 𝑎 ∪ 𝑏 ) ) )
13	12	eqeq1d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 ↔ ( 𝑃 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 ) )
14	13	rexbidv	⊢ ( 𝑝 = 𝑃 → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 ) )
15	14	rabbidv	⊢ ( 𝑝 = 𝑃 → { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 } )
16	15	rspceeqv	⊢ ( ( 𝑃 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 } ) → ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 } )
17	11 16	mpan2	⊢ ( 𝑃 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) → ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 } )
18	17	anim2i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ) → ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 } ) )
19	1 2 3	eldioph4b	⊢ ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } ∈ ( Dioph ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ ∃ 𝑝 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } = { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑝 ‘ ( 𝑎 ∪ 𝑏 ) ) = 0 } ) )
20	18 19	sylibr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ( mzPoly ‘ ( 𝑊 ∪ ( 1 ... 𝑁 ) ) ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ∃ 𝑤 ∈ ( ℕ0 ↑m 𝑊 ) ( 𝑃 ‘ ( 𝑡 ∪ 𝑤 ) ) = 0 } ∈ ( Dioph ‘ 𝑁 ) )