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	$⊢ A \in Dioph (B) \to A \subseteq {ℕ_{0}}^{(1 \dots B)}$

Proof

Step	Hyp	Ref	Expression
1		eldioph3b	$⊢ A \in Dioph (B) \leftrightarrow (B \in ℕ_{0} \land \exists a \in mzPoly (ℕ) A = \{b \| \exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0)\})$
2		simpr	$⊢ ((B \in ℕ_{0} \land a \in mzPoly (ℕ)) \land A = \{b \| \exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0)\}) \to A = \{b \| \exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0)\}$
3		vex	$⊢ d \in V$
4		eqeq1	$⊢ b = d \to (b = {c ↾}_{(1 \dots B)} \leftrightarrow d = {c ↾}_{(1 \dots B)})$
5	4	anbi1d	$⊢ b = d \to ((b = {c ↾}_{(1 \dots B)} \land a (c) = 0) \leftrightarrow (d = {c ↾}_{(1 \dots B)} \land a (c) = 0))$
6	5	rexbidv	$⊢ b = d \to (\exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0) \leftrightarrow \exists c \in ({ℕ_{0}}^{ℕ}) (d = {c ↾}_{(1 \dots B)} \land a (c) = 0))$
7	3 6	elab	$⊢ d \in \{b \| \exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0)\} \leftrightarrow \exists c \in ({ℕ_{0}}^{ℕ}) (d = {c ↾}_{(1 \dots B)} \land a (c) = 0)$
8		simpr	$⊢ (((B \in ℕ_{0} \land a \in mzPoly (ℕ)) \land c \in ({ℕ_{0}}^{ℕ})) \land d = {c ↾}_{(1 \dots B)}) \to d = {c ↾}_{(1 \dots B)}$
9		elfznn	$⊢ a \in (1 \dots B) \to a \in ℕ$
10	9	ssriv	$⊢ (1 \dots B) \subseteq ℕ$
11		elmapssres	$⊢ (c \in ({ℕ_{0}}^{ℕ}) \land (1 \dots B) \subseteq ℕ) \to {c ↾}_{(1 \dots B)} \in ({ℕ_{0}}^{(1 \dots B)})$
12	10 11	mpan2	$⊢ c \in ({ℕ_{0}}^{ℕ}) \to {c ↾}_{(1 \dots B)} \in ({ℕ_{0}}^{(1 \dots B)})$
13	12	ad2antlr	$⊢ (((B \in ℕ_{0} \land a \in mzPoly (ℕ)) \land c \in ({ℕ_{0}}^{ℕ})) \land d = {c ↾}_{(1 \dots B)}) \to {c ↾}_{(1 \dots B)} \in ({ℕ_{0}}^{(1 \dots B)})$
14	8 13	eqeltrd	$⊢ (((B \in ℕ_{0} \land a \in mzPoly (ℕ)) \land c \in ({ℕ_{0}}^{ℕ})) \land d = {c ↾}_{(1 \dots B)}) \to d \in ({ℕ_{0}}^{(1 \dots B)})$
15	14	ex	$⊢ ((B \in ℕ_{0} \land a \in mzPoly (ℕ)) \land c \in ({ℕ_{0}}^{ℕ})) \to (d = {c ↾}_{(1 \dots B)} \to d \in ({ℕ_{0}}^{(1 \dots B)}))$
16	15	adantrd	$⊢ ((B \in ℕ_{0} \land a \in mzPoly (ℕ)) \land c \in ({ℕ_{0}}^{ℕ})) \to ((d = {c ↾}_{(1 \dots B)} \land a (c) = 0) \to d \in ({ℕ_{0}}^{(1 \dots B)}))$
17	16	rexlimdva	$⊢ (B \in ℕ_{0} \land a \in mzPoly (ℕ)) \to (\exists c \in ({ℕ_{0}}^{ℕ}) (d = {c ↾}_{(1 \dots B)} \land a (c) = 0) \to d \in ({ℕ_{0}}^{(1 \dots B)}))$
18	7 17	syl5bi	$⊢ (B \in ℕ_{0} \land a \in mzPoly (ℕ)) \to (d \in \{b \| \exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0)\} \to d \in ({ℕ_{0}}^{(1 \dots B)}))$
19	18	ssrdv	$⊢ (B \in ℕ_{0} \land a \in mzPoly (ℕ)) \to \{b \| \exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0)\} \subseteq {ℕ_{0}}^{(1 \dots B)}$
20	19	adantr	$⊢ ((B \in ℕ_{0} \land a \in mzPoly (ℕ)) \land A = \{b \| \exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0)\}) \to \{b \| \exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0)\} \subseteq {ℕ_{0}}^{(1 \dots B)}$
21	2 20	eqsstrd	$⊢ ((B \in ℕ_{0} \land a \in mzPoly (ℕ)) \land A = \{b \| \exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0)\}) \to A \subseteq {ℕ_{0}}^{(1 \dots B)}$
22	21	r19.29an	$⊢ (B \in ℕ_{0} \land \exists a \in mzPoly (ℕ) A = \{b \| \exists c \in ({ℕ_{0}}^{ℕ}) (b = {c ↾}_{(1 \dots B)} \land a (c) = 0)\}) \to A \subseteq {ℕ_{0}}^{(1 \dots B)}$
23	1 22	sylbi	$⊢ A \in Dioph (B) \to A \subseteq {ℕ_{0}}^{(1 \dots B)}$

Metamath Proof Explorer

Theorem eldiophss

Proof