MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vdwlem13 Unicode version

Theorem vdwlem13 14140
Description: Lemma for vdw 14141. Main induction on ; , base cases. (Contributed by Mario Carneiro, 18-Aug-2014.)
Hypotheses
Ref Expression
vdw.r
vdw.k
Assertion
Ref Expression
vdwlem13
Distinct variable groups:   , ,   , ,   , ,   ,

Proof of Theorem vdwlem13
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elnn1uz2 11016 . . 3
2 vdw.r . . . . . . . . . 10
3 ovex 6199 . . . . . . . . . 10
4 elmapg 7311 . . . . . . . . . 10
52, 3, 4sylancl 662 . . . . . . . . 9
65biimpa 484 . . . . . . . 8
7 1nn 10418 . . . . . . . . . 10
8 vdwap1 14124 . . . . . . . . . 10
97, 7, 8mp2an 672 . . . . . . . . 9
10 1z 10761 . . . . . . . . . . . 12
11 elfz3 11546 . . . . . . . . . . . 12
1210, 11mp1i 12 . . . . . . . . . . 11
13 eqidd 2451 . . . . . . . . . . 11
14 ffn 5641 . . . . . . . . . . . . 13
1514adantl 466 . . . . . . . . . . . 12
16 fniniseg 5907 . . . . . . . . . . . 12
1715, 16syl 16 . . . . . . . . . . 11
1812, 13, 17mpbir2and 913 . . . . . . . . . 10
1918snssd 4100 . . . . . . . . 9
209, 19syl5eqss 3482 . . . . . . . 8
216, 20syldan 470 . . . . . . 7
2221ralrimiva 2879 . . . . . 6
23 fveq2 5773 . . . . . . . . 9
2423oveqd 6191 . . . . . . . 8
2524sseq1d 3465 . . . . . . 7
2625ralbidv 2808 . . . . . 6
2722, 26syl5ibrcom 222 . . . . 5
28 oveq1 6181 . . . . . . . . . . . 12
2928sseq1d 3465 . . . . . . . . . . 11
30 oveq2 6182 . . . . . . . . . . . 12
3130sseq1d 3465 . . . . . . . . . . 11
3229, 31rspc2ev 3162 . . . . . . . . . 10
337, 7, 32mp3an12 1305 . . . . . . . . 9
34 fvex 5783 . . . . . . . . . 10
35 sneq 3969 . . . . . . . . . . . . 13
3635imaeq2d 5251 . . . . . . . . . . . 12
3736sseq2d 3466 . . . . . . . . . . 11
38372rexbidv 2832 . . . . . . . . . 10
3934, 38spcev 3144 . . . . . . . . 9
4033, 39syl 16 . . . . . . . 8
41 vdw.k . . . . . . . . . 10
4241adantr 465 . . . . . . . . 9
433, 42, 6vdwmc 14125 . . . . . . . 8
4440, 43syl5ibr 221 . . . . . . 7
4544ralimdva 2873 . . . . . 6
46 oveq2 6182 . . . . . . . . . 10
4746oveq2d 6190 . . . . . . . . 9
4847raleqdv 3003 . . . . . . . 8
4948rspcev 3153 . . . . . . 7
507, 49mpan 670 . . . . . 6
5145, 50syl6 33 . . . . 5
5227, 51syld 44 . . . 4
53 breq1 4377 . . . . . . . 8
5453rexralbidv 2833 . . . . . . 7
5554ralbidv 2808 . . . . . 6
56 breq1 4377 . . . . . . . 8
5756rexralbidv 2833 . . . . . . 7
5857ralbidv 2808 . . . . . 6
59 breq1 4377 . . . . . . . 8
6059rexralbidv 2833 . . . . . . 7
6160ralbidv 2808 . . . . . 6
62 breq1 4377 . . . . . . . 8
6362rexralbidv 2833 . . . . . . 7
6463ralbidv 2808 . . . . . 6
65 hashcl 12211 . . . . . . . . . 10
66 nn0p1nn 10704 . . . . . . . . . 10
6765, 66syl 16 . . . . . . . . 9
68 simpll 753 . . . . . . . . . . . 12
69 simplr 754 . . . . . . . . . . . . 13
70 vex 3055 . . . . . . . . . . . . . 14
71 ovex 6199 . . . . . . . . . . . . . 14
7270, 71elmap 7325 . . . . . . . . . . . . 13
7369, 72sylib 196 . . . . . . . . . . . 12
74 simpr 461 . . . . . . . . . . . 12
7568, 73, 74vdwlem12 14139 . . . . . . . . . . 11
76 iman 424 . . . . . . . . . . 11
7775, 76mpbir 209 . . . . . . . . . 10
7877ralrimiva 2879 . . . . . . . . 9
79 oveq2 6182 . . . . . . . . . . . 12
8079oveq2d 6190 . . . . . . . . . . 11
8180raleqdv 3003 . . . . . . . . . 10
8281rspcev 3153 . . . . . . . . 9
8367, 78, 82syl2anc 661 . . . . . . . 8
8483rgen 2860 . . . . . . 7
8584a1i 11 . . . . . 6
86 oveq1 6181 . . . . . . . . . . 11
8786raleqdv 3003 . . . . . . . . . 10
8887rexbidv 2809 . . . . . . . . 9
89 oveq2 6182 . . . . . . . . . . . . 13
9089oveq2d 6190 . . . . . . . . . . . 12
9190raleqdv 3003 . . . . . . . . . . 11
92 breq2 4378 . . . . . . . . . . . 12
9392cbvralv 3027 . . . . . . . . . . 11
9491, 93syl6bb 261 . . . . . . . . . 10
9594cbvrexv 3028 . . . . . . . . 9
9688, 95syl6bb 261 . . . . . . . 8
9796cbvralv 3027 . . . . . . 7
98 simplr 754 . . . . . . . . . 10
99 simpll 753 . . . . . . . . . 10
100 simpr 461 . . . . . . . . . . 11
10195ralbii 2812 . . . . . . . . . . 11
102100, 101sylibr 212 . . . . . . . . . 10
10398, 99, 102vdwlem11 14138 . . . . . . . . 9
104103ex 434 . . . . . . . 8
105104ralrimdva 2886 . . . . . . 7
10697, 105syl5bi 217 . . . . . 6
10755, 58, 61, 64, 85, 106uzind4 10997 . . . . 5
108 oveq1 6181 . . . . . . . 8
109108raleqdv 3003 . . . . . . 7
110109rexbidv 2809 . . . . . 6
111110rspcv 3149 . . . . 5
1122, 107, 111syl2im 38 . . . 4
11352, 112jaod 380 . . 3
1141, 113syl5bi 217 . 2
115 fveq2 5773 . . . . . . 7
116115oveqd 6191 . . . . . 6
117 vdwap0 14123 . . . . . . 7
1187, 7, 117mp2an 672 . . . . . 6
119116, 118syl6eq 2506 . . . . 5
120 0ss 3748 . . . . 5
121119, 120syl6eqss 3488 . . . 4
122121ralrimivw 2880 . . 3
123122, 51syl5 32 . 2
124 elnn0 10666 . . 3
12541, 124sylib 196 . 2
126114, 123, 125mpjaod 381 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  =wceq 1370  E.wex 1587  e.wcel 1757  A.wral 2792  E.wrex 2793   cvv 3052  C_wss 3410   c0 3719  {csn 3959   class class class wbr 4374  `'ccnv 4921  "cima 4925  Fnwfn 5495  -->wf 5496  `cfv 5500  (class class class)co 6174   cmap 7298   cfn 7394  0cc0 9367  1c1 9368   caddc 9370   cn 10407  2c2 10456   cn0 10664   cz 10731   cuz 10946   cfz 11522   chash 12188   cvdwa 14112   cvdwm 14113
This theorem is referenced by:  vdw  14141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4485  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456  ax-cnex 9423  ax-resscn 9424  ax-1cn 9425  ax-icn 9426  ax-addcl 9427  ax-addrcl 9428  ax-mulcl 9429  ax-mulrcl 9430  ax-mulcom 9431  ax-addass 9432  ax-mulass 9433  ax-distr 9434  ax-i2m1 9435  ax-1ne0 9436  ax-1rid 9437  ax-rnegex 9438  ax-rrecex 9439  ax-cnre 9440  ax-pre-lttri 9441  ax-pre-lttrn 9442  ax-pre-ltadd 9443  ax-pre-mulgt0 9444
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-pss 3426  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4174  df-int 4211  df-iun 4255  df-br 4375  df-opab 4433  df-mpt 4434  df-tr 4468  df-eprel 4714  df-id 4718  df-po 4723  df-so 4724  df-fr 4761  df-we 4763  df-ord 4804  df-on 4805  df-lim 4806  df-suc 4807  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-om 6561  df-1st 6661  df-2nd 6662  df-recs 6916  df-rdg 6950  df-1o 7004  df-2o 7005  df-oadd 7008  df-er 7185  df-map 7300  df-pm 7301  df-en 7395  df-dom 7396  df-sdom 7397  df-fin 7398  df-card 8194  df-cda 8422  df-pnf 9505  df-mnf 9506  df-xr 9507  df-ltxr 9508  df-le 9509  df-sub 9682  df-neg 9683  df-nn 10408  df-2 10465  df-n0 10665  df-z 10732  df-uz 10947  df-rp 11077  df-fz 11523  df-hash 12189  df-vdwap 14115  df-vdwmc 14116  df-vdwpc 14117
  Copyright terms: Public domain W3C validator