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 
|- ( ( ( a ` 1 ) = ( b ` X ) /\ ( a ` 2 ) = ( b ` Y ) /\ ( a ` 3 ) = ( b ` Z ) ) -> ( ph <-> ps ) )
rabren3dioph.b 
|- X e. ( 1 ... N )
rabren3dioph.c 
|- Y e. ( 1 ... N )
rabren3dioph.d 
|- Z e. ( 1 ... N )
Assertion rabren3dioph 
|- ( ( N e. NN0 /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ph } e. ( Dioph ` 3 ) ) -> { b e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 rabren3dioph.a 
 |-  ( ( ( a ` 1 ) = ( b ` X ) /\ ( a ` 2 ) = ( b ` Y ) /\ ( a ` 3 ) = ( b ` Z ) ) -> ( ph <-> ps ) )
2 rabren3dioph.b 
 |-  X e. ( 1 ... N )
3 rabren3dioph.c 
 |-  Y e. ( 1 ... N )
4 rabren3dioph.d 
 |-  Z e. ( 1 ... N )
5 vex 
 |-  b e. _V
6 tpex 
 |-  { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } e. _V
7 5 6 coex 
 |-  ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) e. _V
8 1ne2 
 |-  1 =/= 2
9 1re 
 |-  1 e. RR
10 1lt3 
 |-  1 < 3
11 9 10 ltneii 
 |-  1 =/= 3
12 2re 
 |-  2 e. RR
13 2lt3 
 |-  2 < 3
14 12 13 ltneii 
 |-  2 =/= 3
15 1ex 
 |-  1 e. _V
16 2ex 
 |-  2 e. _V
17 3ex 
 |-  3 e. _V
18 2 elexi 
 |-  X e. _V
19 3 elexi 
 |-  Y e. _V
20 4 elexi 
 |-  Z e. _V
21 15 16 17 18 19 20 fntp 
 |-  ( ( 1 =/= 2 /\ 1 =/= 3 /\ 2 =/= 3 ) -> { <. 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 e. { 1 , 2 , 3 }
24 fvco2 
 |-  ( ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } Fn { 1 , 2 , 3 } /\ 1 e. { 1 , 2 , 3 } ) -> ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 1 ) = ( b ` ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ` 1 ) ) )
25 22 23 24 mp2an 
 |-  ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 1 ) = ( b ` ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ` 1 ) )
26 15 18 fvtp1 
 |-  ( ( 1 =/= 2 /\ 1 =/= 3 ) -> ( { <. 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 o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 1 ) = ( b ` X )
30 16 tpid2 
 |-  2 e. { 1 , 2 , 3 }
31 fvco2 
 |-  ( ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } Fn { 1 , 2 , 3 } /\ 2 e. { 1 , 2 , 3 } ) -> ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 2 ) = ( b ` ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ` 2 ) ) )
32 22 30 31 mp2an 
 |-  ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 2 ) = ( b ` ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ` 2 ) )
33 16 19 fvtp2 
 |-  ( ( 1 =/= 2 /\ 2 =/= 3 ) -> ( { <. 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 o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 2 ) = ( b ` Y )
37 17 tpid3 
 |-  3 e. { 1 , 2 , 3 }
38 fvco2 
 |-  ( ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } Fn { 1 , 2 , 3 } /\ 3 e. { 1 , 2 , 3 } ) -> ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 3 ) = ( b ` ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ` 3 ) ) )
39 22 37 38 mp2an 
 |-  ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 3 ) = ( b ` ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ` 3 ) )
40 17 20 fvtp3 
 |-  ( ( 1 =/= 3 /\ 2 =/= 3 ) -> ( { <. 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 o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 3 ) = ( b ` Z )
44 29 36 43 3pm3.2i 
 |-  ( ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 1 ) = ( b ` X ) /\ ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 2 ) = ( b ` Y ) /\ ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 3 ) = ( b ` Z ) )
45 fveq1 
 |-  ( a = ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) -> ( a ` 1 ) = ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 1 ) )
46 45 eqeq1d 
 |-  ( a = ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) -> ( ( a ` 1 ) = ( b ` X ) <-> ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 1 ) = ( b ` X ) ) )
47 fveq1 
 |-  ( a = ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) -> ( a ` 2 ) = ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 2 ) )
48 47 eqeq1d 
 |-  ( a = ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) -> ( ( a ` 2 ) = ( b ` Y ) <-> ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 2 ) = ( b ` Y ) ) )
49 fveq1 
 |-  ( a = ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) -> ( a ` 3 ) = ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 3 ) )
50 49 eqeq1d 
 |-  ( a = ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) -> ( ( a ` 3 ) = ( b ` Z ) <-> ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 3 ) = ( b ` Z ) ) )
51 46 48 50 3anbi123d 
 |-  ( a = ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) -> ( ( ( a ` 1 ) = ( b ` X ) /\ ( a ` 2 ) = ( b ` Y ) /\ ( a ` 3 ) = ( b ` Z ) ) <-> ( ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 1 ) = ( b ` X ) /\ ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 2 ) = ( b ` Y ) /\ ( ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) ` 3 ) = ( b ` Z ) ) ) )
52 44 51 mpbiri 
 |-  ( a = ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) -> ( ( a ` 1 ) = ( b ` X ) /\ ( a ` 2 ) = ( b ` Y ) /\ ( a ` 3 ) = ( b ` Z ) ) )
53 52 1 syl 
 |-  ( a = ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) -> ( ph <-> ps ) )
54 7 53 sbcie 
 |-  ( [. ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) / a ]. ph <-> ps )
55 54 rabbii 
 |-  { b e. ( NN0 ^m ( 1 ... N ) ) | [. ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) / a ]. ph } = { b e. ( NN0 ^m ( 1 ... N ) ) | ps }
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 e. ZZ
58 fztp 
 |-  ( 1 e. ZZ -> ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
59 57 58 ax-mp 
 |-  ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
60 1p2e3 
 |-  ( 1 + 2 ) = 3
61 60 oveq2i 
 |-  ( 1 ... ( 1 + 2 ) ) = ( 1 ... 3 )
62 eqidd 
 |-  ( 1 e. ZZ -> 1 = 1 )
63 1p1e2 
 |-  ( 1 + 1 ) = 2
64 63 a1i 
 |-  ( 1 e. ZZ -> ( 1 + 1 ) = 2 )
65 60 a1i 
 |-  ( 1 e. ZZ -> ( 1 + 2 ) = 3 )
66 62 64 65 tpeq123d 
 |-  ( 1 e. ZZ -> { 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 ... 3 ) = { 1 , 2 , 3 }
69 68 feq2i 
 |-  ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } : ( 1 ... 3 ) --> { X , Y , Z } <-> { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } : { 1 , 2 , 3 } --> { X , Y , Z } )
70 56 69 mpbir 
 |-  { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } : ( 1 ... 3 ) --> { X , Y , Z }
71 2 3 4 3pm3.2i 
 |-  ( X e. ( 1 ... N ) /\ Y e. ( 1 ... N ) /\ Z e. ( 1 ... N ) )
72 18 19 20 tpss 
 |-  ( ( X e. ( 1 ... N ) /\ Y e. ( 1 ... N ) /\ Z e. ( 1 ... N ) ) <-> { X , Y , Z } C_ ( 1 ... N ) )
73 71 72 mpbi 
 |-  { X , Y , Z } C_ ( 1 ... N )
74 fss 
 |-  ( ( { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } : ( 1 ... 3 ) --> { X , Y , Z } /\ { X , Y , Z } C_ ( 1 ... N ) ) -> { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } : ( 1 ... 3 ) --> ( 1 ... N ) )
75 70 73 74 mp2an 
 |-  { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } : ( 1 ... 3 ) --> ( 1 ... N )
76 rabrenfdioph 
 |-  ( ( N e. NN0 /\ { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } : ( 1 ... 3 ) --> ( 1 ... N ) /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ph } e. ( Dioph ` 3 ) ) -> { b e. ( NN0 ^m ( 1 ... N ) ) | [. ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) / a ]. ph } e. ( Dioph ` N ) )
77 75 76 mp3an2 
 |-  ( ( N e. NN0 /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ph } e. ( Dioph ` 3 ) ) -> { b e. ( NN0 ^m ( 1 ... N ) ) | [. ( b o. { <. 1 , X >. , <. 2 , Y >. , <. 3 , Z >. } ) / a ]. ph } e. ( Dioph ` N ) )
78 55 77 eqeltrrid 
 |-  ( ( N e. NN0 /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ph } e. ( Dioph ` 3 ) ) -> { b e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) )