Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  diophren Unicode version

Theorem diophren 26044
 Description: Change variables in a Diophantine set, using class notation. This allows already proved Diophantine sets to be reused in contexts with more variables. (Contributed by Stefan O'Rear, 16-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
Assertion
Ref Expression
diophren Dioph Dioph
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem diophren
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zex 10080 . . . . . 6
2 difexg 4199 . . . . . 6
31, 2ax-mp 8 . . . . 5
4 ominf 7118 . . . . . 6
5 nnuz 10310 . . . . . . . . . 10
6 0p1e1 9884 . . . . . . . . . . 11
76fveq2i 5566 . . . . . . . . . 10
85, 7eqtr4i 2339 . . . . . . . . 9
98difeq2i 3325 . . . . . . . 8
10 0z 10082 . . . . . . . . 9
11 lzenom 25997 . . . . . . . . 9
1210, 11ax-mp 8 . . . . . . . 8
139, 12eqbrtri 4079 . . . . . . 7
14 enfi 7122 . . . . . . 7
1513, 14ax-mp 8 . . . . . 6
164, 15mtbir 290 . . . . 5
17 incom 3395 . . . . . 6
18 disjdif 3560 . . . . . 6
1917, 18eqtri 2336 . . . . 5
203, 16, 19eldioph4b 26042 . . . 4 Dioph mzPoly
21 simpr 447 . . . . . . . . . . . 12 mzPoly
22 simplr 731 . . . . . . . . . . . . 13
2322ad2antrr 706 . . . . . . . . . . . 12 mzPoly
24 ovex 5925 . . . . . . . . . . . . 13
2524mapco2 25939 . . . . . . . . . . . 12
2621, 23, 25syl2anc 642 . . . . . . . . . . 11 mzPoly
27 uneq1 3356 . . . . . . . . . . . . . . 15
2827fveq2d 5567 . . . . . . . . . . . . . 14
2928eqeq1d 2324 . . . . . . . . . . . . 13
3029rexbidv 2598 . . . . . . . . . . . 12
3130elrab3 2958 . . . . . . . . . . 11
3226, 31syl 15 . . . . . . . . . 10 mzPoly
3322ad3antrrr 710 . . . . . . . . . . . . . . 15 mzPoly
34 simplr 731 . . . . . . . . . . . . . . 15 mzPoly
35 simpr 447 . . . . . . . . . . . . . . 15 mzPoly
36 coundi 5211 . . . . . . . . . . . . . . . 16
37 coundir 5212 . . . . . . . . . . . . . . . . . . 19
38 elmapi 6835 . . . . . . . . . . . . . . . . . . . . . 22
39383ad2ant3 978 . . . . . . . . . . . . . . . . . . . . 21
40 simp1 955 . . . . . . . . . . . . . . . . . . . . 21
41 incom 3395 . . . . . . . . . . . . . . . . . . . . . . 23
42 fz1ssnn 26040 . . . . . . . . . . . . . . . . . . . . . . . 24
43 ssdisj 3538 . . . . . . . . . . . . . . . . . . . . . . . 24
4442, 18, 43mp2an 653 . . . . . . . . . . . . . . . . . . . . . . 23
4541, 44eqtri 2336 . . . . . . . . . . . . . . . . . . . . . 22
4645a1i 10 . . . . . . . . . . . . . . . . . . . . 21
47 coeq0i 25980 . . . . . . . . . . . . . . . . . . . . 21
4839, 40, 46, 47syl3anc 1182 . . . . . . . . . . . . . . . . . . . 20
4948uneq2d 3363 . . . . . . . . . . . . . . . . . . 19
5037, 49syl5eq 2360 . . . . . . . . . . . . . . . . . 18
51 un0 3513 . . . . . . . . . . . . . . . . . 18
5250, 51syl6eq 2364 . . . . . . . . . . . . . . . . 17
53 coundir 5212 . . . . . . . . . . . . . . . . . . 19
54 elmapi 6835 . . . . . . . . . . . . . . . . . . . . . 22
55543ad2ant2 977 . . . . . . . . . . . . . . . . . . . . 21
56 f1oi 5549 . . . . . . . . . . . . . . . . . . . . . . 23
57 f1of 5510 . . . . . . . . . . . . . . . . . . . . . . 23
5856, 57ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22
59 coeq0i 25980 . . . . . . . . . . . . . . . . . . . . . 22
6058, 44, 59mp3an23 1269 . . . . . . . . . . . . . . . . . . . . 21
6155, 60syl 15 . . . . . . . . . . . . . . . . . . . 20
62 coires1 5227 . . . . . . . . . . . . . . . . . . . . . 22
63 ffn 5427 . . . . . . . . . . . . . . . . . . . . . . 23
64 fnresdm 5390 . . . . . . . . . . . . . . . . . . . . . . 23
6538, 63, 643syl 18 . . . . . . . . . . . . . . . . . . . . . 22
6662, 65syl5eq 2360 . . . . . . . . . . . . . . . . . . . . 21
67663ad2ant3 978 . . . . . . . . . . . . . . . . . . . 20
6861, 67uneq12d 3364 . . . . . . . . . . . . . . . . . . 19
6953, 68syl5eq 2360 . . . . . . . . . . . . . . . . . 18
70 uncom 3353 . . . . . . . . . . . . . . . . . . 19
71 un0 3513 . . . . . . . . . . . . . . . . . . 19
7270, 71eqtri 2336 . . . . . . . . . . . . . . . . . 18
7369, 72syl6eq 2364 . . . . . . . . . . . . . . . . 17
7452, 73uneq12d 3364 . . . . . . . . . . . . . . . 16
7536, 74syl5req 2361 . . . . . . . . . . . . . . 15
7633, 34, 35, 75syl3anc 1182 . . . . . . . . . . . . . 14 mzPoly
7776fveq2d 5567 . . . . . . . . . . . . 13 mzPoly
78 nn0ssz 10091 . . . . . . . . . . . . . . . . 17
79 mapss 6853 . . . . . . . . . . . . . . . . 17
801, 78, 79mp2an 653 . . . . . . . . . . . . . . . 16
8144reseq2i 4989 . . . . . . . . . . . . . . . . . . 19
82 res0 4996 . . . . . . . . . . . . . . . . . . 19
8381, 82eqtri 2336 . . . . . . . . . . . . . . . . . 18
8444reseq2i 4989 . . . . . . . . . . . . . . . . . . 19
85 res0 4996 . . . . . . . . . . . . . . . . . . 19
8684, 85eqtri 2336 . . . . . . . . . . . . . . . . . 18
8783, 86eqtr4i 2339 . . . . . . . . . . . . . . . . 17
88 elmapresaun 25998 . . . . . . . . . . . . . . . . . 18
89 uncom 3353 . . . . . . . . . . . . . . . . . . 19
9089oveq2i 5911 . . . . . . . . . . . . . . . . . 18
9188, 90syl6eleq 2406 . . . . . . . . . . . . . . . . 17
9287, 91mp3an3 1266 . . . . . . . . . . . . . . . 16
9380, 92sseldi 3212 . . . . . . . . . . . . . . 15
9493adantll 694 . . . . . . . . . . . . . 14 mzPoly
95 coeq1 4878 . . . . . . . . . . . . . . . 16
9695fveq2d 5567 . . . . . . . . . . . . . . 15
97 eqid 2316 . . . . . . . . . . . . . . 15
98 fvex 5577 . . . . . . . . . . . . . . 15
9996, 97, 98fvmpt 5640 . . . . . . . . . . . . . 14
10094, 99syl 15 . . . . . . . . . . . . 13 mzPoly
10177, 100eqtr4d 2351 . . . . . . . . . . . 12 mzPoly
102101eqeq1d 2324 . . . . . . . . . . 11 mzPoly
103102rexbidva 2594 . . . . . . . . . 10 mzPoly
10432, 103bitrd 244 . . . . . . . . 9 mzPoly
105104rabbidva 2813 . . . . . . . 8 mzPoly
106 simplll 734 . . . . . . . . 9 mzPoly
107 ovex 5925 . . . . . . . . . . . 12
1083, 107unex 4555 . . . . . . . . . . 11
109108a1i 10 . . . . . . . . . 10 mzPoly
110 simpr 447 . . . . . . . . . 10 mzPoly mzPoly
111 simpllr 735 . . . . . . . . . . 11 mzPoly
11258a1i 10 . . . . . . . . . . . . 13
113 id 19 . . . . . . . . . . . . 13
114 incom 3395 . . . . . . . . . . . . . . 15
115 fz1ssnn 26040 . . . . . . . . . . . . . . . 16
116 ssdisj 3538 . . . . . . . . . . . . . . . 16
117115, 18, 116mp2an 653 . . . . . . . . . . . . . . 15
118114, 117eqtri 2336 . . . . . . . . . . . . . 14
119118a1i 10 . . . . . . . . . . . . 13
120 fun 5443 . . . . . . . . . . . . 13
121112, 113, 119, 120syl21anc 1181 . . . . . . . . . . . 12
122 uncom 3353 . . . . . . . . . . . . 13
123122feq1i 5421 . . . . . . . . . . . 12
124121, 123sylib 188 . . . . . . . . . . 11
125111, 124syl 15 . . . . . . . . . 10 mzPoly
126 mzprename 25975 . . . . . . . . . 10 mzPoly mzPoly
127109, 110, 125, 126syl3anc 1182 . . . . . . . . 9 mzPoly mzPoly
1283, 16, 19eldioph4i 26043 . . . . . . . . 9 mzPoly Dioph
129106, 127, 128syl2anc 642 . . . . . . . 8 mzPoly Dioph
130105, 129eqeltrd 2390 . . . . . . 7 mzPoly Dioph
131 eleq2 2377 . . . . . . . . 9
132131rabbidv 2814 . . . . . . . 8
133132eleq1d 2382 . . . . . . 7 Dioph Dioph
134130, 133syl5ibrcom 213 . . . . . 6 mzPoly Dioph
135134rexlimdva 2701 . . . . 5 mzPoly Dioph
136135expimpd 586 . . . 4 mzPoly Dioph
13720, 136syl5bi 208 . . 3 Dioph Dioph
138137impcom 419 . 2 Dioph Dioph
1391383impb 1147 1 Dioph Dioph
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1633   wcel 1701  wrex 2578  crab 2581  cvv 2822   cdif 3183   cun 3184   cin 3185   wss 3186  c0 3489   class class class wbr 4060   cmpt 4114   cid 4341  com 4693   cres 4728   ccom 4730   wfn 5287  wf 5288  wf1o 5291  cfv 5292  (class class class)co 5900   cmap 6815   cen 6903  cfn 6906  cc0 8782  c1 8783   caddc 8785  cn 9791  cn0 10012  cz 10071  cuz 10277  cfz 10829  mzPolycmzp 25948  Diophcdioph 25982 This theorem is referenced by:  rabrenfdioph  26045 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-inf2 7387  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-of 6120  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-1o 6521  df-oadd 6525  df-er 6702  df-map 6817  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-card 7617  df-cda 7839  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-nn 9792  df-n0 10013  df-z 10072  df-uz 10278  df-fz 10830  df-hash 11385  df-mzpcl 25949  df-mzp 25950  df-dioph 25983
 Copyright terms: Public domain W3C validator