eldiophb

Description: Initial expression of Diophantine property of a set. (Contributed by Stefan O'Rear, 5-Oct-2014) (Revised by Mario Carneiro, 22-Sep-2015)

		Ref	Expression
	Assertion	eldiophb	$⊢ D \in Dioph (N) \leftrightarrow (N \in ℕ_{0} \land \exists k \in ℤ_{\geq N} \exists p \in mzPoly ((1 \dots k)) D = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$

Proof

Step	Hyp	Ref	Expression
1		df-dioph	$⊢ Dioph = (n \in ℕ_{0} ⟼ ran (k \in ℤ_{\geq n}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots n)} \land p (u) = 0)\}))$
2	1	dmmptss	$⊢ dom Dioph \subseteq ℕ_{0}$
3		elfvdm	$⊢ D \in Dioph (N) \to N \in dom Dioph$
4	2 3	sseldi	$⊢ D \in Dioph (N) \to N \in ℕ_{0}$
5		fveq2	$⊢ n = N \to ℤ_{\geq n} = ℤ_{\geq N}$
6		eqidd	$⊢ n = N \to mzPoly ((1 \dots k)) = mzPoly ((1 \dots k))$
7		oveq2	$⊢ n = N \to (1 \dots n) = (1 \dots N)$
8	7	reseq2d	$⊢ n = N \to {u ↾}_{(1 \dots n)} = {u ↾}_{(1 \dots N)}$
9	8	eqeq2d	$⊢ n = N \to (t = {u ↾}_{(1 \dots n)} \leftrightarrow t = {u ↾}_{(1 \dots N)})$
10	9	anbi1d	$⊢ n = N \to ((t = {u ↾}_{(1 \dots n)} \land p (u) = 0) \leftrightarrow (t = {u ↾}_{(1 \dots N)} \land p (u) = 0))$
11	10	rexbidv	$⊢ n = N \to (\exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots n)} \land p (u) = 0) \leftrightarrow \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0))$
12	11	abbidv	$⊢ n = N \to \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots n)} \land p (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
13	5 6 12	mpoeq123dv	$⊢ n = N \to (k \in ℤ_{\geq n}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots n)} \land p (u) = 0)\}) = (k \in ℤ_{\geq N}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
14	13	rneqd	$⊢ n = N \to ran (k \in ℤ_{\geq n}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots n)} \land p (u) = 0)\}) = ran (k \in ℤ_{\geq N}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
15		ovex	$⊢ {ℕ_{0}}^{(1 \dots N)} \in V$
16	15	pwex	$⊢ 𝒫 ({ℕ_{0}}^{(1 \dots N)}) \in V$
17		eqid	$⊢ (k \in ℤ_{\geq N}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}) = (k \in ℤ_{\geq N}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
18	17	rnmpo	$⊢ ran (k \in ℤ_{\geq N}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}) = \{d \| \exists k \in ℤ_{\geq N} \exists p \in mzPoly ((1 \dots k)) d = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}\}$
19		elmapi	$⊢ u \in ({ℕ_{0}}^{(1 \dots k)}) \to u : (1 \dots k) ⟶ ℕ_{0}$
20		fzss2	$⊢ k \in ℤ_{\geq N} \to (1 \dots N) \subseteq (1 \dots k)$
21		fssres	$⊢ (u : (1 \dots k) ⟶ ℕ_{0} \land (1 \dots N) \subseteq (1 \dots k)) \to ({u ↾}_{(1 \dots N)}) : (1 \dots N) ⟶ ℕ_{0}$
22	19 20 21	syl2anr	$⊢ (k \in ℤ_{\geq N} \land u \in ({ℕ_{0}}^{(1 \dots k)})) \to ({u ↾}_{(1 \dots N)}) : (1 \dots N) ⟶ ℕ_{0}$
23		nn0ex	$⊢ ℕ_{0} \in V$
24		ovex	$⊢ (1 \dots N) \in V$
25	23 24	elmap	$⊢ {u ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)}) \leftrightarrow ({u ↾}_{(1 \dots N)}) : (1 \dots N) ⟶ ℕ_{0}$
26	22 25	sylibr	$⊢ (k \in ℤ_{\geq N} \land u \in ({ℕ_{0}}^{(1 \dots k)})) \to {u ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)})$
27		eleq1	$⊢ t = {u ↾}_{(1 \dots N)} \to (t \in ({ℕ_{0}}^{(1 \dots N)}) \leftrightarrow {u ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)}))$
28	27	adantr	$⊢ (t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \to (t \in ({ℕ_{0}}^{(1 \dots N)}) \leftrightarrow {u ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)}))$
29	26 28	syl5ibrcom	$⊢ (k \in ℤ_{\geq N} \land u \in ({ℕ_{0}}^{(1 \dots k)})) \to ((t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \to t \in ({ℕ_{0}}^{(1 \dots N)}))$
30	29	rexlimdva	$⊢ k \in ℤ_{\geq N} \to (\exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \to t \in ({ℕ_{0}}^{(1 \dots N)}))$
31	30	abssdv	$⊢ k \in ℤ_{\geq N} \to \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \subseteq {ℕ_{0}}^{(1 \dots N)}$
32	15	elpw2	$⊢ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \in 𝒫 ({ℕ_{0}}^{(1 \dots N)}) \leftrightarrow \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \subseteq {ℕ_{0}}^{(1 \dots N)}$
33	31 32	sylibr	$⊢ k \in ℤ_{\geq N} \to \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \in 𝒫 ({ℕ_{0}}^{(1 \dots N)})$
34		eleq1	$⊢ d = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \to (d \in 𝒫 ({ℕ_{0}}^{(1 \dots N)}) \leftrightarrow \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \in 𝒫 ({ℕ_{0}}^{(1 \dots N)}))$
35	33 34	syl5ibrcom	$⊢ k \in ℤ_{\geq N} \to (d = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \to d \in 𝒫 ({ℕ_{0}}^{(1 \dots N)}))$
36	35	rexlimdvw	$⊢ k \in ℤ_{\geq N} \to (\exists p \in mzPoly ((1 \dots k)) d = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \to d \in 𝒫 ({ℕ_{0}}^{(1 \dots N)}))$
37	36	rexlimiv	$⊢ \exists k \in ℤ_{\geq N} \exists p \in mzPoly ((1 \dots k)) d = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \to d \in 𝒫 ({ℕ_{0}}^{(1 \dots N)})$
38	37	abssi	$⊢ \{d \| \exists k \in ℤ_{\geq N} \exists p \in mzPoly ((1 \dots k)) d = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}\} \subseteq 𝒫 ({ℕ_{0}}^{(1 \dots N)})$
39	18 38	eqsstri	$⊢ ran (k \in ℤ_{\geq N}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}) \subseteq 𝒫 ({ℕ_{0}}^{(1 \dots N)})$
40	16 39	ssexi	$⊢ ran (k \in ℤ_{\geq N}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}) \in V$
41	14 1 40	fvmpt	$⊢ N \in ℕ_{0} \to Dioph (N) = ran (k \in ℤ_{\geq N}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
42	41	eleq2d	$⊢ N \in ℕ_{0} \to (D \in Dioph (N) \leftrightarrow D \in ran (k \in ℤ_{\geq N}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}))$
43		ovex	$⊢ {ℕ_{0}}^{(1 \dots k)} \in V$
44	43	abrexex	$⊢ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) t = {u ↾}_{(1 \dots N)}\} \in V$
45		simpl	$⊢ (t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \to t = {u ↾}_{(1 \dots N)}$
46	45	reximi	$⊢ \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \to \exists u \in ({ℕ_{0}}^{(1 \dots k)}) t = {u ↾}_{(1 \dots N)}$
47	46	ss2abi	$⊢ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \subseteq \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) t = {u ↾}_{(1 \dots N)}\}$
48	44 47	ssexi	$⊢ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \in V$
49	17 48	elrnmpo	$⊢ D \in ran (k \in ℤ_{\geq N}, p \in mzPoly ((1 \dots k)) ⟼ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}) \leftrightarrow \exists k \in ℤ_{\geq N} \exists p \in mzPoly ((1 \dots k)) D = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
50	42 49	bitrdi	$⊢ N \in ℕ_{0} \to (D \in Dioph (N) \leftrightarrow \exists k \in ℤ_{\geq N} \exists p \in mzPoly ((1 \dots k)) D = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
51	4 50	biadanii	$⊢ D \in Dioph (N) \leftrightarrow (N \in ℕ_{0} \land \exists k \in ℤ_{\geq N} \exists p \in mzPoly ((1 \dots k)) D = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$

Metamath Proof Explorer

Theorem eldiophb

Proof