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

Theorem hashdom 11991
Description: Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 22-Apr-2015.)
Assertion
Ref Expression
hashdom

Proof of Theorem hashdom
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfi 11643 . . . . . . . 8
2 ficardom 8017 . . . . . . . 8
31, 2ax-mp 5 . . . . . . 7
4 eqid 2489 . . . . . . . . . . . . . 14
54hashgval 11955 . . . . . . . . . . . . 13
65ad2antrr 708 . . . . . . . . . . . 12
74hashgval 11955 . . . . . . . . . . . . . 14
81, 7ax-mp 5 . . . . . . . . . . . . 13
9 hashcl 11975 . . . . . . . . . . . . . . . 16
109ad2antrr 708 . . . . . . . . . . . . . . 15
11 hashcl 11975 . . . . . . . . . . . . . . . 16
1211ad2antlr 709 . . . . . . . . . . . . . . 15
13 simpr 449 . . . . . . . . . . . . . . 15
14 nn0sub2 10569 . . . . . . . . . . . . . . 15
1510, 12, 13, 14syl3anc 1192 . . . . . . . . . . . . . 14
16 hashfz1 11966 . . . . . . . . . . . . . 14
1715, 16syl 16 . . . . . . . . . . . . 13
188, 17syl5eq 2533 . . . . . . . . . . . 12
196, 18oveq12d 6121 . . . . . . . . . . 11
209nn0cnd 10502 . . . . . . . . . . . . 13
2111nn0cnd 10502 . . . . . . . . . . . . 13
22 pncan3 9495 . . . . . . . . . . . . 13
2320, 21, 22syl2an 465 . . . . . . . . . . . 12
2423adantr 453 . . . . . . . . . . 11
2519, 24eqtrd 2521 . . . . . . . . . 10
26 ficardom 8017 . . . . . . . . . . . 12
2726ad2antrr 708 . . . . . . . . . . 11
284hashgadd 11989 . . . . . . . . . . 11
2927, 3, 28sylancl 645 . . . . . . . . . 10
304hashgval 11955 . . . . . . . . . . 11
3130ad2antlr 709 . . . . . . . . . 10
3225, 29, 313eqtr4d 2531 . . . . . . . . 9
3332fveq2d 5712 . . . . . . . 8
344hashgf1o 11642 . . . . . . . . 9
35 nnacl 7016 . . . . . . . . . 10
3627, 3, 35sylancl 645 . . . . . . . . 9
37 f1ocnvfv1 5995 . . . . . . . . 9
3834, 36, 37sylancr 646 . . . . . . . 8
39 ficardom 8017 . . . . . . . . . 10
4039ad2antlr 709 . . . . . . . . 9
41 f1ocnvfv1 5995 . . . . . . . . 9
4234, 40, 41sylancr 646 . . . . . . . 8
4333, 38, 423eqtr3d 2529 . . . . . . 7
44 oveq2 6111 . . . . . . . . 9
4544eqeq1d 2497 . . . . . . . 8
4645rspcev 3113 . . . . . . 7
473, 43, 46sylancr 646 . . . . . 6
4847ex 425 . . . . 5
49 cardnn 8019 . . . . . . . . . 10
5049adantl 454 . . . . . . . . 9
5150oveq2d 6119 . . . . . . . 8
5251eqeq1d 2497 . . . . . . 7
53 fveq2 5708 . . . . . . . 8
54 nnfi 7464 . . . . . . . . 9
55 ficardom 8017 . . . . . . . . . . . . . 14
564hashgadd 11989 . . . . . . . . . . . . . 14
5726, 55, 56syl2an 465 . . . . . . . . . . . . 13
584hashgval 11955 . . . . . . . . . . . . . 14
595, 58oveqan12d 6122 . . . . . . . . . . . . 13
6057, 59eqtrd 2521 . . . . . . . . . . . 12
6160adantlr 697 . . . . . . . . . . 11
6230ad2antlr 709 . . . . . . . . . . 11
6361, 62eqeq12d 2503 . . . . . . . . . 10
64 hashcl 11975 . . . . . . . . . . . . . . 15
6564nn0ge0d 10503 . . . . . . . . . . . . . 14
6665adantl 454 . . . . . . . . . . . . 13
679nn0red 10501 . . . . . . . . . . . . . 14
6864nn0red 10501 . . . . . . . . . . . . . 14
69 addge01 9723 . . . . . . . . . . . . . 14
7067, 68, 69syl2an 465 . . . . . . . . . . . . 13
7166, 70mpbid 203 . . . . . . . . . . . 12
7271adantlr 697 . . . . . . . . . . 11
73 breq2 4322 . . . . . . . . . . 11
7472, 73syl5ibcom 213 . . . . . . . . . 10
7563, 74sylbid 208 . . . . . . . . 9
7654, 75sylan2 462 . . . . . . . 8
7753, 76syl5 31 . . . . . . 7
7852, 77sylbird 228 . . . . . 6
7978rexlimdva 2884 . . . . 5
8048, 79impbid 185 . . . 4
81 nnawordex 7042 . . . . 5
8226, 39, 81syl2an 465 . . . 4
83 finnum 8004 . . . . 5
84 finnum 8004 . . . . 5
85 carddom2 8033 . . . . 5
8683, 84, 85syl2an 465 . . . 4
8780, 82, 863bitr2d 274 . . 3
8887adantlr 697 . 2
89 hashxrcl 11976 . . . . . 6
9089ad2antrr 708 . . . . 5
91 pnfge 10974 . . . . 5
9290, 91syl 16 . . . 4
93 hashinf 11957 . . . . 5
9493adantll 696 . . . 4
9592, 94breqtrrd 4344 . . 3
96 isinffi 8048 . . . . . 6
9796ancoms 441 . . . . 5
9897adantlr 697 . . . 4
99 brdomg 7282 . . . . 5
10099ad2antlr 709 . . . 4
10198, 100mpbird 225 . . 3
10295, 1012thd 233 . 2
10388, 102pm2.61dan 768 1
Colors of variables: wff set class
Syntax hints:  -.wn 3  ->wi 4  <->wb 178  /\wa 360  E.wex 1565  =wceq 1670  e.wcel 1732  E.wrex 2760   cvv 3015  C_wss 3365   class class class wbr 4318  e.cmpt 4376  `'ccnv 4861  domcdm 4862  |`cres 4864  -1-1->wf1 5435  -1-1-onto->wf1o 5437  `cfv 5438  (class class class)co 6103   com 6486  reccrdg 6829   coa 6883   cdom 7271   cfn 7273   ccrd 7991   cc 9159   cr 9160  0cc0 9161  1c1 9162   caddc 9164   cpnf 9294   cxr 9296   cle 9298   cmin 9472   cn0 10445   cfz 11293   chash 11952
This theorem is referenced by:  hashdomi  11992  hashsdom  11993  hashun2  11995  hashss  12015  hashsslei  12025  hashfun  12046  hashf1  12057  isercoll  12992  phicl2  13690  phibnd  13693  prmreclem2  13825  prmreclem3  13826  4sqlem11  13863  vdwlem11  13899  ramub2  13922  0ram  13928  ram0  13930  sylow1lem4  15844  pgpssslw  15857  fislw  15868  znfld  17466  znidomb  17467  fta1blem  21106  birthdaylem3  21813  basellem4  21887  ppiwordi  21966  musum  21997  ppiub  22009  chpub  22025  lgsqrlem4  22149  umgraex  22379  sizeusglecusg  22516  konigsberg  22730  derangenlem  26205  subfaclefac  26210  erdsze2lem1  26237  snmlff  26364  idomsubgmo  28745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382  ax-cnex 9217  ax-resscn 9218  ax-1cn 9219  ax-icn 9220  ax-addcl 9221  ax-addrcl 9222  ax-mulcl 9223  ax-mulrcl 9224  ax-mulcom 9225  ax-addass 9226  ax-mulass 9227  ax-distr 9228  ax-i2m1 9229  ax-1ne0 9230  ax-1rid 9231  ax-rnegex 9232  ax-rrecex 9233  ax-cnre 9234  ax-pre-lttri 9235  ax-pre-lttrn 9236  ax-pre-ltadd 9237  ax-pre-mulgt0 9238
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-nel 2655  df-ral 2764  df-rex 2765  df-reu 2766  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-pss 3381  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-tp 3917  df-op 3918  df-uni 4118  df-int 4155  df-iun 4199  df-br 4319  df-opab 4377  df-mpt 4378  df-tr 4412  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-fv 5446  df-riota 6062  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-om 6487  df-1st 6583  df-2nd 6584  df-recs 6795  df-rdg 6830  df-1o 6886  df-oadd 6890  df-er 7067  df-en 7274  df-dom 7275  df-sdom 7276  df-fin 7277  df-card 7995  df-pnf 9299  df-mnf 9300  df-xr 9301  df-ltxr 9302  df-le 9303  df-sub 9474  df-neg 9475  df-nn 10189  df-n0 10446  df-z 10511  df-uz 10726  df-fz 11294  df-hash 11953
  Copyright terms: Public domain W3C validator