Metamath Proof Explorer


Theorem 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 a1=bXa2=bYa3=bZφψ
rabren3dioph.b X1N
rabren3dioph.c Y1N
rabren3dioph.d Z1N
Assertion rabren3dioph N0a013|φDioph3b01N|ψDiophN

Proof

Step Hyp Ref Expression
1 rabren3dioph.a a1=bXa2=bYa3=bZφψ
2 rabren3dioph.b X1N
3 rabren3dioph.c Y1N
4 rabren3dioph.d Z1N
5 vex bV
6 tpex 1X2Y3ZV
7 5 6 coex b1X2Y3ZV
8 1ne2 12
9 1re 1
10 1lt3 1<3
11 9 10 ltneii 13
12 2re 2
13 2lt3 2<3
14 12 13 ltneii 23
15 1ex 1V
16 2ex 2V
17 3ex 3V
18 2 elexi XV
19 3 elexi YV
20 4 elexi ZV
21 15 16 17 18 19 20 fntp 1213231X2Y3ZFn123
22 8 11 14 21 mp3an 1X2Y3ZFn123
23 15 tpid1 1123
24 fvco2 1X2Y3ZFn1231123b1X2Y3Z1=b1X2Y3Z1
25 22 23 24 mp2an b1X2Y3Z1=b1X2Y3Z1
26 15 18 fvtp1 12131X2Y3Z1=X
27 8 11 26 mp2an 1X2Y3Z1=X
28 27 fveq2i b1X2Y3Z1=bX
29 25 28 eqtri b1X2Y3Z1=bX
30 16 tpid2 2123
31 fvco2 1X2Y3ZFn1232123b1X2Y3Z2=b1X2Y3Z2
32 22 30 31 mp2an b1X2Y3Z2=b1X2Y3Z2
33 16 19 fvtp2 12231X2Y3Z2=Y
34 8 14 33 mp2an 1X2Y3Z2=Y
35 34 fveq2i b1X2Y3Z2=bY
36 32 35 eqtri b1X2Y3Z2=bY
37 17 tpid3 3123
38 fvco2 1X2Y3ZFn1233123b1X2Y3Z3=b1X2Y3Z3
39 22 37 38 mp2an b1X2Y3Z3=b1X2Y3Z3
40 17 20 fvtp3 13231X2Y3Z3=Z
41 11 14 40 mp2an 1X2Y3Z3=Z
42 41 fveq2i b1X2Y3Z3=bZ
43 39 42 eqtri b1X2Y3Z3=bZ
44 29 36 43 3pm3.2i b1X2Y3Z1=bXb1X2Y3Z2=bYb1X2Y3Z3=bZ
45 fveq1 a=b1X2Y3Za1=b1X2Y3Z1
46 45 eqeq1d a=b1X2Y3Za1=bXb1X2Y3Z1=bX
47 fveq1 a=b1X2Y3Za2=b1X2Y3Z2
48 47 eqeq1d a=b1X2Y3Za2=bYb1X2Y3Z2=bY
49 fveq1 a=b1X2Y3Za3=b1X2Y3Z3
50 49 eqeq1d a=b1X2Y3Za3=bZb1X2Y3Z3=bZ
51 46 48 50 3anbi123d a=b1X2Y3Za1=bXa2=bYa3=bZb1X2Y3Z1=bXb1X2Y3Z2=bYb1X2Y3Z3=bZ
52 44 51 mpbiri a=b1X2Y3Za1=bXa2=bYa3=bZ
53 52 1 syl a=b1X2Y3Zφψ
54 7 53 sbcie [˙b1X2Y3Z/a]˙φψ
55 54 rabbii b01N|[˙b1X2Y3Z/a]˙φ=b01N|ψ
56 15 16 17 18 19 20 8 11 14 ftp 1X2Y3Z:123XYZ
57 1z 1
58 fztp 111+2=11+11+2
59 57 58 ax-mp 11+2=11+11+2
60 1p2e3 1+2=3
61 60 oveq2i 11+2=13
62 eqidd 11=1
63 1p1e2 1+1=2
64 63 a1i 11+1=2
65 60 a1i 11+2=3
66 62 64 65 tpeq123d 111+11+2=123
67 57 66 ax-mp 11+11+2=123
68 59 61 67 3eqtr3i 13=123
69 68 feq2i 1X2Y3Z:13XYZ1X2Y3Z:123XYZ
70 56 69 mpbir 1X2Y3Z:13XYZ
71 2 3 4 3pm3.2i X1NY1NZ1N
72 18 19 20 tpss X1NY1NZ1NXYZ1N
73 71 72 mpbi XYZ1N
74 fss 1X2Y3Z:13XYZXYZ1N1X2Y3Z:131N
75 70 73 74 mp2an 1X2Y3Z:131N
76 rabrenfdioph N01X2Y3Z:131Na013|φDioph3b01N|[˙b1X2Y3Z/a]˙φDiophN
77 75 76 mp3an2 N0a013|φDioph3b01N|[˙b1X2Y3Z/a]˙φDiophN
78 55 77 eqeltrrid N0a013|φDioph3b01N|ψDiophN