rexrabdioph

Description: Diophantine set builder for existential quantification. (Contributed by Stefan O'Rear, 10-Oct-2014)

	Ref	Expression
Hypotheses	rexrabdioph.1	$⊢ M = N + 1$
	rexrabdioph.2	$⊢ v = t (M) \to (ψ \leftrightarrow χ)$
	rexrabdioph.3	$⊢ u = {t ↾}_{(1 \dots N)} \to (χ \leftrightarrow φ)$
Assertion	rexrabdioph	$⊢ (N \in ℕ_{0} \land \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} \in Dioph (M)) \to \{u \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists v \in ℕ_{0} ψ\} \in Dioph (N)$

Proof

Step	Hyp	Ref	Expression
1		rexrabdioph.1	$⊢ M = N + 1$
2		rexrabdioph.2	$⊢ v = t (M) \to (ψ \leftrightarrow χ)$
3		rexrabdioph.3	$⊢ u = {t ↾}_{(1 \dots N)} \to (χ \leftrightarrow φ)$
4		df-rab	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ\} = \{a \| (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)\}$
5		dfsbcq	$⊢ b = c \to (\underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)$
6	5	cbvrexvw	$⊢ \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ \leftrightarrow \exists c \in ℕ_{0} \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ$
7	6	anbi2i	$⊢ (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ) \leftrightarrow (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists c \in ℕ_{0} \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)$
8		r19.42v	$⊢ \exists c \in ℕ_{0} (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ) \leftrightarrow (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists c \in ℕ_{0} \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)$
9	7 8	bitr4i	$⊢ (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ) \leftrightarrow \exists c \in ℕ_{0} (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)$
10		simpll	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to N \in ℕ_{0}$
11		simpr	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to a \in ({ℕ_{0}}^{(1 \dots N)})$
12		simplr	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to c \in ℕ_{0}$
13	1	mapfzcons	$⊢ (N \in ℕ_{0} \land a \in ({ℕ_{0}}^{(1 \dots N)}) \land c \in ℕ_{0}) \to a \cup \{⟨M, c⟩\} \in ({ℕ_{0}}^{(1 \dots M)})$
14	10 11 12 13	syl3anc	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to a \cup \{⟨M, c⟩\} \in ({ℕ_{0}}^{(1 \dots M)})$
15	14	adantrr	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)) \to a \cup \{⟨M, c⟩\} \in ({ℕ_{0}}^{(1 \dots M)})$
16	1	mapfzcons2	$⊢ (a \in ({ℕ_{0}}^{(1 \dots N)}) \land c \in ℕ_{0}) \to (a \cup \{⟨M, c⟩\}) (M) = c$
17	11 12 16	syl2anc	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to (a \cup \{⟨M, c⟩\}) (M) = c$
18	17	eqcomd	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to c = (a \cup \{⟨M, c⟩\}) (M)$
19	1	mapfzcons1	$⊢ a \in ({ℕ_{0}}^{(1 \dots N)}) \to {(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)} = a$
20	19	adantl	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to {(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)} = a$
21	20	eqcomd	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to a = {(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}$
22	21	sbceq1d	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to (\underset{˙}{[} a / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} ({(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ)$
23	18 22	sbceqbid	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to (\underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} (a \cup \{⟨M, c⟩\}) (M) / v \underset{˙}{]} \underset{˙}{[} ({(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ)$
24	23	biimpd	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land a \in ({ℕ_{0}}^{(1 \dots N)})) \to (\underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ \to \underset{˙}{[} (a \cup \{⟨M, c⟩\}) (M) / v \underset{˙}{]} \underset{˙}{[} ({(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ)$
25	24	impr	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)) \to \underset{˙}{[} (a \cup \{⟨M, c⟩\}) (M) / v \underset{˙}{]} \underset{˙}{[} ({(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ$
26	21	adantrr	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)) \to a = {(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}$
27		fveq1	$⊢ b = a \cup \{⟨M, c⟩\} \to b (M) = (a \cup \{⟨M, c⟩\}) (M)$
28		reseq1	$⊢ b = a \cup \{⟨M, c⟩\} \to {b ↾}_{(1 \dots N)} = {(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}$
29	28	sbceq1d	$⊢ b = a \cup \{⟨M, c⟩\} \to (\underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} ({(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ)$
30	27 29	sbceqbid	$⊢ b = a \cup \{⟨M, c⟩\} \to (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} (a \cup \{⟨M, c⟩\}) (M) / v \underset{˙}{]} \underset{˙}{[} ({(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ)$
31	28	eqeq2d	$⊢ b = a \cup \{⟨M, c⟩\} \to (a = {b ↾}_{(1 \dots N)} \leftrightarrow a = {(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)})$
32	30 31	anbi12d	$⊢ b = a \cup \{⟨M, c⟩\} \to ((\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow (\underset{˙}{[} (a \cup \{⟨M, c⟩\}) (M) / v \underset{˙}{]} \underset{˙}{[} ({(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}))$
33	32	rspcev	$⊢ (a \cup \{⟨M, c⟩\} \in ({ℕ_{0}}^{(1 \dots M)}) \land (\underset{˙}{[} (a \cup \{⟨M, c⟩\}) (M) / v \underset{˙}{]} \underset{˙}{[} ({(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {(a \cup \{⟨M, c⟩\}) ↾}_{(1 \dots N)})) \to \exists b \in ({ℕ_{0}}^{(1 \dots M)}) (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})$
34	15 25 26 33	syl12anc	$⊢ ((N \in ℕ_{0} \land c \in ℕ_{0}) \land (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)) \to \exists b \in ({ℕ_{0}}^{(1 \dots M)}) (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})$
35	34	rexlimdva2	$⊢ N \in ℕ_{0} \to (\exists c \in ℕ_{0} (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ) \to \exists b \in ({ℕ_{0}}^{(1 \dots M)}) (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)}))$
36		elmapi	$⊢ b \in ({ℕ_{0}}^{(1 \dots M)}) \to b : (1 \dots M) ⟶ ℕ_{0}$
37		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
38	1 37	eqeltrid	$⊢ N \in ℕ_{0} \to M \in ℕ$
39		elfz1end	$⊢ M \in ℕ \leftrightarrow M \in (1 \dots M)$
40	38 39	sylib	$⊢ N \in ℕ_{0} \to M \in (1 \dots M)$
41		ffvelrn	$⊢ (b : (1 \dots M) ⟶ ℕ_{0} \land M \in (1 \dots M)) \to b (M) \in ℕ_{0}$
42	36 40 41	syl2anr	$⊢ (N \in ℕ_{0} \land b \in ({ℕ_{0}}^{(1 \dots M)})) \to b (M) \in ℕ_{0}$
43	42	adantr	$⊢ ((N \in ℕ_{0} \land b \in ({ℕ_{0}}^{(1 \dots M)})) \land (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})) \to b (M) \in ℕ_{0}$
44		simprr	$⊢ ((N \in ℕ_{0} \land b \in ({ℕ_{0}}^{(1 \dots M)})) \land (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})) \to a = {b ↾}_{(1 \dots N)}$
45	1	mapfzcons1cl	$⊢ b \in ({ℕ_{0}}^{(1 \dots M)}) \to {b ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)})$
46	45	ad2antlr	$⊢ ((N \in ℕ_{0} \land b \in ({ℕ_{0}}^{(1 \dots M)})) \land (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})) \to {b ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)})$
47	44 46	eqeltrd	$⊢ ((N \in ℕ_{0} \land b \in ({ℕ_{0}}^{(1 \dots M)})) \land (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})) \to a \in ({ℕ_{0}}^{(1 \dots N)})$
48		simprl	$⊢ ((N \in ℕ_{0} \land b \in ({ℕ_{0}}^{(1 \dots M)})) \land (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})) \to \underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ$
49		dfsbcq	$⊢ a = {b ↾}_{(1 \dots N)} \to (\underset{˙}{[} a / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ)$
50	49	sbcbidv	$⊢ a = {b ↾}_{(1 \dots N)} \to (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ)$
51	50	ad2antll	$⊢ ((N \in ℕ_{0} \land b \in ({ℕ_{0}}^{(1 \dots M)})) \land (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})) \to (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ)$
52	48 51	mpbird	$⊢ ((N \in ℕ_{0} \land b \in ({ℕ_{0}}^{(1 \dots M)})) \land (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})) \to \underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ$
53		dfsbcq	$⊢ c = b (M) \to (\underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)$
54	53	anbi2d	$⊢ c = b (M) \to ((a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ) \leftrightarrow (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ))$
55	54	rspcev	$⊢ (b (M) \in ℕ_{0} \land (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)) \to \exists c \in ℕ_{0} (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)$
56	43 47 52 55	syl12anc	$⊢ ((N \in ℕ_{0} \land b \in ({ℕ_{0}}^{(1 \dots M)})) \land (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})) \to \exists c \in ℕ_{0} (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)$
57	56	rexlimdva2	$⊢ N \in ℕ_{0} \to (\exists b \in ({ℕ_{0}}^{(1 \dots M)}) (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)}) \to \exists c \in ℕ_{0} (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ))$
58	35 57	impbid	$⊢ N \in ℕ_{0} \to (\exists c \in ℕ_{0} (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \underset{˙}{[} c / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ) \leftrightarrow \exists b \in ({ℕ_{0}}^{(1 \dots M)}) (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)}))$
59	9 58	syl5bb	$⊢ N \in ℕ_{0} \to ((a \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ) \leftrightarrow \exists b \in ({ℕ_{0}}^{(1 \dots M)}) (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)}))$
60	59	abbidv	$⊢ N \in ℕ_{0} \to \{a \| (a \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)\} = \{a \| \exists b \in ({ℕ_{0}}^{(1 \dots M)}) (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})\}$
61	4 60	syl5eq	$⊢ N \in ℕ_{0} \to \{a \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ\} = \{a \| \exists b \in ({ℕ_{0}}^{(1 \dots M)}) (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})\}$
62		nfcv	$⊢ \underline{Ⅎ} u ({ℕ_{0}}^{(1 \dots N)})$
63		nfcv	$⊢ \underline{Ⅎ} a ({ℕ_{0}}^{(1 \dots N)})$
64		nfv	$⊢ Ⅎ a \exists v \in ℕ_{0} ψ$
65		nfcv	$⊢ \underline{Ⅎ} u ℕ_{0}$
66		nfcv	$⊢ \underline{Ⅎ} u b$
67		nfsbc1v	$⊢ Ⅎ u \underset{˙}{[} a / u \underset{˙}{]} ψ$
68	66 67	nfsbcw	$⊢ Ⅎ u \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ$
69	65 68	nfrex	$⊢ Ⅎ u \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ$
70		sbceq1a	$⊢ u = a \to (ψ \leftrightarrow \underset{˙}{[} a / u \underset{˙}{]} ψ)$
71	70	rexbidv	$⊢ u = a \to (\exists v \in ℕ_{0} ψ \leftrightarrow \exists v \in ℕ_{0} \underset{˙}{[} a / u \underset{˙}{]} ψ)$
72		nfv	$⊢ Ⅎ b \underset{˙}{[} a / u \underset{˙}{]} ψ$
73		nfsbc1v	$⊢ Ⅎ v \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ$
74		sbceq1a	$⊢ v = b \to (\underset{˙}{[} a / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)$
75	72 73 74	cbvrexw	$⊢ \exists v \in ℕ_{0} \underset{˙}{[} a / u \underset{˙}{]} ψ \leftrightarrow \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ$
76	71 75	bitrdi	$⊢ u = a \to (\exists v \in ℕ_{0} ψ \leftrightarrow \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ)$
77	62 63 64 69 76	cbvrabw	$⊢ \{u \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists v \in ℕ_{0} ψ\} = \{a \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} \underset{˙}{[} b / v \underset{˙}{]} \underset{˙}{[} a / u \underset{˙}{]} ψ\}$
78		fveq1	$⊢ t = b \to t (M) = b (M)$
79		reseq1	$⊢ t = b \to {t ↾}_{(1 \dots N)} = {b ↾}_{(1 \dots N)}$
80	79	sbceq1d	$⊢ t = b \to (\underset{˙}{[} ({t ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ)$
81	78 80	sbceqbid	$⊢ t = b \to (\underset{˙}{[} t (M) / v \underset{˙}{]} \underset{˙}{[} ({t ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ)$
82	81	rexrab	$⊢ \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| \underset{˙}{[} t (M) / v \underset{˙}{]} \underset{˙}{[} ({t ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ\} a = {b ↾}_{(1 \dots N)} \leftrightarrow \exists b \in ({ℕ_{0}}^{(1 \dots M)}) (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})$
83	82	abbii	$⊢ \{a \| \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| \underset{˙}{[} t (M) / v \underset{˙}{]} \underset{˙}{[} ({t ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ\} a = {b ↾}_{(1 \dots N)}\} = \{a \| \exists b \in ({ℕ_{0}}^{(1 \dots M)}) (\underset{˙}{[} b (M) / v \underset{˙}{]} \underset{˙}{[} ({b ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \land a = {b ↾}_{(1 \dots N)})\}$
84	61 77 83	3eqtr4g	$⊢ N \in ℕ_{0} \to \{u \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists v \in ℕ_{0} ψ\} = \{a \| \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| \underset{˙}{[} t (M) / v \underset{˙}{]} \underset{˙}{[} ({t ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ\} a = {b ↾}_{(1 \dots N)}\}$
85		fvex	$⊢ t (M) \in V$
86		vex	$⊢ t \in V$
87	86	resex	$⊢ {t ↾}_{(1 \dots N)} \in V$
88	2 3	sylan9bb	$⊢ (v = t (M) \land u = {t ↾}_{(1 \dots N)}) \to (ψ \leftrightarrow φ)$
89	85 87 88	sbc2ie	$⊢ \underset{˙}{[} t (M) / v \underset{˙}{]} \underset{˙}{[} ({t ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ \leftrightarrow φ$
90	89	rabbii	$⊢ \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| \underset{˙}{[} t (M) / v \underset{˙}{]} \underset{˙}{[} ({t ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ\} = \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\}$
91	90	rexeqi	$⊢ \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| \underset{˙}{[} t (M) / v \underset{˙}{]} \underset{˙}{[} ({t ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ\} a = {b ↾}_{(1 \dots N)} \leftrightarrow \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} a = {b ↾}_{(1 \dots N)}$
92	91	abbii	$⊢ \{a \| \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| \underset{˙}{[} t (M) / v \underset{˙}{]} \underset{˙}{[} ({t ↾}_{(1 \dots N)}) / u \underset{˙}{]} ψ\} a = {b ↾}_{(1 \dots N)}\} = \{a \| \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} a = {b ↾}_{(1 \dots N)}\}$
93	84 92	eqtrdi	$⊢ N \in ℕ_{0} \to \{u \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists v \in ℕ_{0} ψ\} = \{a \| \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} a = {b ↾}_{(1 \dots N)}\}$
94	93	adantr	$⊢ (N \in ℕ_{0} \land \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} \in Dioph (M)) \to \{u \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists v \in ℕ_{0} ψ\} = \{a \| \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} a = {b ↾}_{(1 \dots N)}\}$
95		simpl	$⊢ (N \in ℕ_{0} \land \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} \in Dioph (M)) \to N \in ℕ_{0}$
96		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
97		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
98		peano2uz	$⊢ N \in ℤ_{\geq N} \to N + 1 \in ℤ_{\geq N}$
99	96 97 98	3syl	$⊢ N \in ℕ_{0} \to N + 1 \in ℤ_{\geq N}$
100	1 99	eqeltrid	$⊢ N \in ℕ_{0} \to M \in ℤ_{\geq N}$
101	100	adantr	$⊢ (N \in ℕ_{0} \land \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} \in Dioph (M)) \to M \in ℤ_{\geq N}$
102		simpr	$⊢ (N \in ℕ_{0} \land \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} \in Dioph (M)) \to \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} \in Dioph (M)$
103		diophrex	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} \in Dioph (M)) \to \{a \| \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} a = {b ↾}_{(1 \dots N)}\} \in Dioph (N)$
104	95 101 102 103	syl3anc	$⊢ (N \in ℕ_{0} \land \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} \in Dioph (M)) \to \{a \| \exists b \in \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} a = {b ↾}_{(1 \dots N)}\} \in Dioph (N)$
105	94 104	eqeltrd	$⊢ (N \in ℕ_{0} \land \{t \in ({ℕ_{0}}^{(1 \dots M)}) \| φ\} \in Dioph (M)) \to \{u \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists v \in ℕ_{0} ψ\} \in Dioph (N)$

Metamath Proof Explorer

Theorem rexrabdioph

Proof