rabren3dioph

Description: Change variable numbers in a 3-variable Diophantine class abstraction. (Contributed by Stefan O'Rear, 17-Oct-2014)

	Ref	Expression
Hypotheses	rabren3dioph.a	$⊢ (a (1) = b (X) \land a (2) = b (Y) \land a (3) = b (Z)) \to (φ \leftrightarrow ψ)$
	rabren3dioph.b	$⊢ X \in (1 \dots N)$
	rabren3dioph.c	$⊢ Y \in (1 \dots N)$
	rabren3dioph.d	$⊢ Z \in (1 \dots N)$
Assertion	rabren3dioph	$⊢ (N \in ℕ_{0} \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| φ\} \in Dioph (3)) \to \{b \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N)$

Proof

Step	Hyp	Ref	Expression
1		rabren3dioph.a	$⊢ (a (1) = b (X) \land a (2) = b (Y) \land a (3) = b (Z)) \to (φ \leftrightarrow ψ)$
2		rabren3dioph.b	$⊢ X \in (1 \dots N)$
3		rabren3dioph.c	$⊢ Y \in (1 \dots N)$
4		rabren3dioph.d	$⊢ Z \in (1 \dots N)$
5		vex	$⊢ b \in V$
6		tpex	$⊢ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \in V$
7	5 6	coex	$⊢ b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \in V$
8		1ne2	$⊢ 1 \neq 2$
9		1re	$⊢ 1 \in ℝ$
10		1lt3	$⊢ 1 < 3$
11	9 10	ltneii	$⊢ 1 \neq 3$
12		2re	$⊢ 2 \in ℝ$
13		2lt3	$⊢ 2 < 3$
14	12 13	ltneii	$⊢ 2 \neq 3$
15		1ex	$⊢ 1 \in V$
16		2ex	$⊢ 2 \in V$
17		3ex	$⊢ 3 \in V$
18	2	elexi	$⊢ X \in V$
19	3	elexi	$⊢ Y \in V$
20	4	elexi	$⊢ Z \in V$
21	15 16 17 18 19 20	fntp	$⊢ (1 \neq 2 \land 1 \neq 3 \land 2 \neq 3) \to \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} Fn \{1, 2, 3\}$
22	8 11 14 21	mp3an	$⊢ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} Fn \{1, 2, 3\}$
23	15	tpid1	$⊢ 1 \in \{1, 2, 3\}$
24		fvco2	$⊢ (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} Fn \{1, 2, 3\} \land 1 \in \{1, 2, 3\}) \to (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (1) = b (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (1))$
25	22 23 24	mp2an	$⊢ (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (1) = b (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (1))$
26	15 18	fvtp1	$⊢ (1 \neq 2 \land 1 \neq 3) \to \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (1) = X$
27	8 11 26	mp2an	$⊢ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (1) = X$
28	27	fveq2i	$⊢ b (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (1)) = b (X)$
29	25 28	eqtri	$⊢ (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (1) = b (X)$
30	16	tpid2	$⊢ 2 \in \{1, 2, 3\}$
31		fvco2	$⊢ (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} Fn \{1, 2, 3\} \land 2 \in \{1, 2, 3\}) \to (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (2) = b (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (2))$
32	22 30 31	mp2an	$⊢ (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (2) = b (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (2))$
33	16 19	fvtp2	$⊢ (1 \neq 2 \land 2 \neq 3) \to \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (2) = Y$
34	8 14 33	mp2an	$⊢ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (2) = Y$
35	34	fveq2i	$⊢ b (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (2)) = b (Y)$
36	32 35	eqtri	$⊢ (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (2) = b (Y)$
37	17	tpid3	$⊢ 3 \in \{1, 2, 3\}$
38		fvco2	$⊢ (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} Fn \{1, 2, 3\} \land 3 \in \{1, 2, 3\}) \to (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (3) = b (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (3))$
39	22 37 38	mp2an	$⊢ (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (3) = b (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (3))$
40	17 20	fvtp3	$⊢ (1 \neq 3 \land 2 \neq 3) \to \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (3) = Z$
41	11 14 40	mp2an	$⊢ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (3) = Z$
42	41	fveq2i	$⊢ b (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} (3)) = b (Z)$
43	39 42	eqtri	$⊢ (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (3) = b (Z)$
44	29 36 43	3pm3.2i	$⊢ ((b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (1) = b (X) \land (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (2) = b (Y) \land (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (3) = b (Z))$
45		fveq1	$⊢ a = b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \to a (1) = (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (1)$
46	45	eqeq1d	$⊢ a = b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \to (a (1) = b (X) \leftrightarrow (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (1) = b (X))$
47		fveq1	$⊢ a = b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \to a (2) = (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (2)$
48	47	eqeq1d	$⊢ a = b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \to (a (2) = b (Y) \leftrightarrow (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (2) = b (Y))$
49		fveq1	$⊢ a = b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \to a (3) = (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (3)$
50	49	eqeq1d	$⊢ a = b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \to (a (3) = b (Z) \leftrightarrow (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (3) = b (Z))$
51	46 48 50	3anbi123d	$⊢ a = b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \to ((a (1) = b (X) \land a (2) = b (Y) \land a (3) = b (Z)) \leftrightarrow ((b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (1) = b (X) \land (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (2) = b (Y) \land (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) (3) = b (Z)))$
52	44 51	mpbiri	$⊢ a = b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \to (a (1) = b (X) \land a (2) = b (Y) \land a (3) = b (Z))$
53	52 1	syl	$⊢ a = b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} \to (φ \leftrightarrow ψ)$
54	7 53	sbcie	$⊢ \underset{˙}{[} (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) / a \underset{˙}{]} φ \leftrightarrow ψ$
55	54	rabbii	$⊢ \{b \in ({ℕ_{0}}^{(1 \dots N)}) \| \underset{˙}{[} (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) / a \underset{˙}{]} φ\} = \{b \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\}$
56	15 16 17 18 19 20 8 11 14	ftp	$⊢ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} : \{1, 2, 3\} ⟶ \{X, Y, Z\}$
57		1z	$⊢ 1 \in ℤ$
58		fztp	$⊢ 1 \in ℤ \to (1 \dots 1 + 2) = \{1, 1 + 1, 1 + 2\}$
59	57 58	ax-mp	$⊢ (1 \dots 1 + 2) = \{1, 1 + 1, 1 + 2\}$
60		1p2e3	$⊢ 1 + 2 = 3$
61	60	oveq2i	$⊢ (1 \dots 1 + 2) = (1 \dots 3)$
62		eqidd	$⊢ 1 \in ℤ \to 1 = 1$
63		1p1e2	$⊢ 1 + 1 = 2$
64	63	a1i	$⊢ 1 \in ℤ \to 1 + 1 = 2$
65	60	a1i	$⊢ 1 \in ℤ \to 1 + 2 = 3$
66	62 64 65	tpeq123d	$⊢ 1 \in ℤ \to \{1, 1 + 1, 1 + 2\} = \{1, 2, 3\}$
67	57 66	ax-mp	$⊢ \{1, 1 + 1, 1 + 2\} = \{1, 2, 3\}$
68	59 61 67	3eqtr3i	$⊢ (1 \dots 3) = \{1, 2, 3\}$
69	68	feq2i	$⊢ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} : (1 \dots 3) ⟶ \{X, Y, Z\} \leftrightarrow \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} : \{1, 2, 3\} ⟶ \{X, Y, Z\}$
70	56 69	mpbir	$⊢ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} : (1 \dots 3) ⟶ \{X, Y, Z\}$
71	2 3 4	3pm3.2i	$⊢ (X \in (1 \dots N) \land Y \in (1 \dots N) \land Z \in (1 \dots N))$
72	18 19 20	tpss	$⊢ (X \in (1 \dots N) \land Y \in (1 \dots N) \land Z \in (1 \dots N)) \leftrightarrow \{X, Y, Z\} \subseteq (1 \dots N)$
73	71 72	mpbi	$⊢ \{X, Y, Z\} \subseteq (1 \dots N)$
74		fss	$⊢ (\{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} : (1 \dots 3) ⟶ \{X, Y, Z\} \land \{X, Y, Z\} \subseteq (1 \dots N)) \to \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} : (1 \dots 3) ⟶ (1 \dots N)$
75	70 73 74	mp2an	$⊢ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} : (1 \dots 3) ⟶ (1 \dots N)$
76		rabrenfdioph	$⊢ (N \in ℕ_{0} \land \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\} : (1 \dots 3) ⟶ (1 \dots N) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| φ\} \in Dioph (3)) \to \{b \in ({ℕ_{0}}^{(1 \dots N)}) \| \underset{˙}{[} (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) / a \underset{˙}{]} φ\} \in Dioph (N)$
77	75 76	mp3an2	$⊢ (N \in ℕ_{0} \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| φ\} \in Dioph (3)) \to \{b \in ({ℕ_{0}}^{(1 \dots N)}) \| \underset{˙}{[} (b \circ \{⟨1, X⟩, ⟨2, Y⟩, ⟨3, Z⟩\}) / a \underset{˙}{]} φ\} \in Dioph (N)$
78	55 77	eqeltrrid	$⊢ (N \in ℕ_{0} \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| φ\} \in Dioph (3)) \to \{b \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N)$

Metamath Proof Explorer

Theorem rabren3dioph

Proof