Theorem eldiophss

Description: Diophantine sets are sets of tuples of nonnegative integers. (Contributed by Stefan O'Rear, 10-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

	Ref	Expression
Assertion	eldiophss	⊢ ( 𝐴 ∈ ( Dioph ‘ 𝐵 ) → 𝐴 ⊆ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldioph3b	⊢ ( 𝐴 ∈ ( Dioph ‘ 𝐵 ) ↔ ( 𝐵 ∈ ℕ0 ∧ ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) } ) )
2		simpr	⊢ ( ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝐴 = { 𝑏 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) } ) → 𝐴 = { 𝑏 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) } )
3		vex	⊢ 𝑑 ∈ V
4		eqeq1	⊢ ( 𝑏 = 𝑑 → ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ↔ 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ) )
5	4	anbi1d	⊢ ( 𝑏 = 𝑑 → ( ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) ↔ ( 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) ) )
6	5	rexbidv	⊢ ( 𝑏 = 𝑑 → ( ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) ↔ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) ) )
7	3 6	elab	⊢ ( 𝑑 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) } ↔ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) )
8		simpr	⊢ ( ( ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ) ∧ 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ) → 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) )
9		elfznn	⊢ ( 𝑎 ∈ ( 1 ... 𝐵 ) → 𝑎 ∈ ℕ )
10	9	ssriv	⊢ ( 1 ... 𝐵 ) ⊆ ℕ
11		elmapssres	⊢ ( ( 𝑐 ∈ ( ℕ0 ↑m ℕ ) ∧ ( 1 ... 𝐵 ) ⊆ ℕ ) → ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) )
12	10 11	mpan2	⊢ ( 𝑐 ∈ ( ℕ0 ↑m ℕ ) → ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) )
13	12	ad2antlr	⊢ ( ( ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ) ∧ 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ) → ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) )
14	8 13	eqeltrd	⊢ ( ( ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ) ∧ 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ) → 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) )
15	14	ex	⊢ ( ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ) → ( 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) → 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ) )
16	15	adantrd	⊢ ( ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ) → ( ( 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) → 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ) )
17	16	rexlimdva	⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) → ( ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑑 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) → 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ) )
18	7 17	syl5bi	⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) → ( 𝑑 ∈ { 𝑏 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) } → 𝑑 ∈ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) ) )
19	18	ssrdv	⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) → { 𝑏 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) } ⊆ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) )
20	19	adantr	⊢ ( ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝐴 = { 𝑏 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) } ) → { 𝑏 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) } ⊆ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) )
21	2 20	eqsstrd	⊢ ( ( ( 𝐵 ∈ ℕ0 ∧ 𝑎 ∈ ( mzPoly ‘ ℕ ) ) ∧ 𝐴 = { 𝑏 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) } ) → 𝐴 ⊆ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) )
22	21	r19.29an	⊢ ( ( 𝐵 ∈ ℕ0 ∧ ∃ 𝑎 ∈ ( mzPoly ‘ ℕ ) 𝐴 = { 𝑏 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m ℕ ) ( 𝑏 = ( 𝑐 ↾ ( 1 ... 𝐵 ) ) ∧ ( 𝑎 ‘ 𝑐 ) = 0 ) } ) → 𝐴 ⊆ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) )
23	1 22	sylbi	⊢ ( 𝐴 ∈ ( Dioph ‘ 𝐵 ) → 𝐴 ⊆ ( ℕ0 ↑m ( 1 ... 𝐵 ) ) )