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

Theorem hashdom 11934
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 11586 . . . . . . . 8
2 ficardom 7962 . . . . . . . 8
31, 2ax-mp 5 . . . . . . 7
4 eqid 2481 . . . . . . . . . . . . . 14
54hashgval 11898 . . . . . . . . . . . . 13
65ad2antrr 708 . . . . . . . . . . . 12
74hashgval 11898 . . . . . . . . . . . . . 14
81, 7ax-mp 5 . . . . . . . . . . . . 13
9 hashcl 11918 . . . . . . . . . . . . . . . 16
109ad2antrr 708 . . . . . . . . . . . . . . 15
11 hashcl 11918 . . . . . . . . . . . . . . . 16
1211ad2antlr 709 . . . . . . . . . . . . . . 15
13 simpr 449 . . . . . . . . . . . . . . 15
14 nn0sub2 10512 . . . . . . . . . . . . . . 15
1510, 12, 13, 14syl3anc 1192 . . . . . . . . . . . . . 14
16 hashfz1 11909 . . . . . . . . . . . . . 14
1715, 16syl 16 . . . . . . . . . . . . 13
188, 17syl5eq 2525 . . . . . . . . . . . 12
196, 18oveq12d 6085 . . . . . . . . . . 11
209nn0cnd 10445 . . . . . . . . . . . . 13
2111nn0cnd 10445 . . . . . . . . . . . . 13
22 pncan3 9438 . . . . . . . . . . . . 13
2320, 21, 22syl2an 465 . . . . . . . . . . . 12
2423adantr 453 . . . . . . . . . . 11
2519, 24eqtrd 2513 . . . . . . . . . 10
26 ficardom 7962 . . . . . . . . . . . 12
2726ad2antrr 708 . . . . . . . . . . 11
284hashgadd 11932 . . . . . . . . . . 11
2927, 3, 28sylancl 645 . . . . . . . . . 10
304hashgval 11898 . . . . . . . . . . 11
3130ad2antlr 709 . . . . . . . . . 10
3225, 29, 313eqtr4d 2523 . . . . . . . . 9
3332fveq2d 5689 . . . . . . . 8
344hashgf1o 11585 . . . . . . . . 9
35 nnacl 6966 . . . . . . . . . 10
3627, 3, 35sylancl 645 . . . . . . . . 9
37 f1ocnvfv1 5959 . . . . . . . . 9
3834, 36, 37sylancr 646 . . . . . . . 8
39 ficardom 7962 . . . . . . . . . 10
4039ad2antlr 709 . . . . . . . . 9
41 f1ocnvfv1 5959 . . . . . . . . 9
4234, 40, 41sylancr 646 . . . . . . . 8
4333, 38, 423eqtr3d 2521 . . . . . . 7
44 oveq2 6075 . . . . . . . . 9
4544eqeq1d 2489 . . . . . . . 8
4645rspcev 3102 . . . . . . 7
473, 43, 46sylancr 646 . . . . . 6
4847ex 425 . . . . 5
49 cardnn 7964 . . . . . . . . . 10
5049adantl 454 . . . . . . . . 9
5150oveq2d 6083 . . . . . . . 8
5251eqeq1d 2489 . . . . . . 7
53 fveq2 5685 . . . . . . . 8
54 nnfi 7411 . . . . . . . . 9
55 ficardom 7962 . . . . . . . . . . . . . 14
564hashgadd 11932 . . . . . . . . . . . . . 14
5726, 55, 56syl2an 465 . . . . . . . . . . . . 13
584hashgval 11898 . . . . . . . . . . . . . 14
595, 58oveqan12d 6086 . . . . . . . . . . . . 13
6057, 59eqtrd 2513 . . . . . . . . . . . 12
6160adantlr 697 . . . . . . . . . . 11
6230ad2antlr 709 . . . . . . . . . . 11
6361, 62eqeq12d 2495 . . . . . . . . . 10
64 hashcl 11918 . . . . . . . . . . . . . . 15
6564nn0ge0d 10446 . . . . . . . . . . . . . 14
6665adantl 454 . . . . . . . . . . . . 13
679nn0red 10444 . . . . . . . . . . . . . 14
6864nn0red 10444 . . . . . . . . . . . . . 14
69 addge01 9666 . . . . . . . . . . . . . 14
7067, 68, 69syl2an 465 . . . . . . . . . . . . 13
7166, 70mpbid 203 . . . . . . . . . . . 12
7271adantlr 697 . . . . . . . . . . 11
73 breq2 4306 . . . . . . . . . . 11
7472, 73syl5ibcom 213 . . . . . . . . . 10
7563, 74sylbid 208 . . . . . . . . 9
7654, 75sylan2 462 . . . . . . . 8
7753, 76syl5 31 . . . . . . 7
7852, 77sylbird 228 . . . . . 6
7978rexlimdva 2876 . . . . 5
8048, 79impbid 185 . . . 4
81 nnawordex 6992 . . . . 5
8226, 39, 81syl2an 465 . . . 4
83 finnum 7949 . . . . 5
84 finnum 7949 . . . . 5
85 carddom2 7978 . . . . 5
8683, 84, 85syl2an 465 . . . 4
8780, 82, 863bitr2d 274 . . 3
8887adantlr 697 . 2
89 hashxrcl 11919 . . . . . 6
9089ad2antrr 708 . . . . 5
91 pnfge 10917 . . . . 5
9290, 91syl 16 . . . 4
93 hashinf 11900 . . . . 5
9493adantll 696 . . . 4
9592, 94breqtrrd 4328 . . 3
96 isinffi 7993 . . . . . 6
9796ancoms 441 . . . . 5
9897adantlr 697 . . . 4
99 brdomg 7230 . . . . 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 1557  =wceq 1662  e.wcel 1724  E.wrex 2752   cvv 3006  C_wss 3353   class class class wbr 4302  e.cmpt 4360  `'ccnv 4843  domcdm 4844  |`cres 4846  -1-1->wf1 5414  -1-1-onto->wf1o 5416  `cfv 5417  (class class class)co 6067   com 6441  reccrdg 6779   coa 6833   cdom 7219   cfn 7221   ccrd 7936   cc 9102   cr 9103  0cc0 9104  1c1 9105   caddc 9107   cpnf 9237   cxr 9239   cle 9241   cmin 9415   cn0 10388   cfz 11236   chash 11895
This theorem is referenced by:  hashdomi  11935  hashsdom  11936  hashun2  11938  hashss  11958  hashsslei  11968  hashfun  11986  hashf1  11997  isercoll  12931  phicl2  13629  phibnd  13632  prmreclem2  13764  prmreclem3  13765  4sqlem11  13802  vdwlem11  13838  ramub2  13861  0ram  13867  ram0  13869  sylow1lem4  15738  pgpssslw  15751  fislw  15762  znfld  17344  znidomb  17345  fta1blem  20595  birthdaylem3  21301  basellem4  21375  ppiwordi  21454  musum  21485  ppiub  21497  chpub  21513  lgsqrlem4  21637  umgraex  21867  sizeusglecusg  22004  konigsberg  22218  derangenlem  25696  subfaclefac  25701  erdsze2lem1  25728  snmlff  25855  idomsubgmo  28420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538  ax-un 6338  ax-cnex 9160  ax-resscn 9161  ax-1cn 9162  ax-icn 9163  ax-addcl 9164  ax-addrcl 9165  ax-mulcl 9166  ax-mulrcl 9167  ax-mulcom 9168  ax-addass 9169  ax-mulass 9170  ax-distr 9171  ax-i2m1 9172  ax-1ne0 9173  ax-1rid 9174  ax-rnegex 9175  ax-rrecex 9176  ax-cnre 9177  ax-pre-lttri 9178  ax-pre-lttrn 9179  ax-pre-ltadd 9180  ax-pre-mulgt0 9181
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-nel 2647  df-ral 2756  df-rex 2757  df-reu 2758  df-rab 2760  df-v 3008  df-sbc 3213  df-csb 3314  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-pss 3369  df-nul 3661  df-if 3813  df-pw 3880  df-sn 3900  df-pr 3901  df-tp 3902  df-op 3903  df-uni 4102  df-int 4139  df-iun 4183  df-br 4303  df-opab 4361  df-mpt 4362  df-tr 4396  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-riota 6026  df-ov 6070  df-oprab 6071  df-mpt2 6072  df-om 6442  df-1st 6538  df-2nd 6539  df-recs 6745  df-rdg 6780  df-1o 6836  df-oadd 6840  df-er 7017  df-en 7222  df-dom 7223  df-sdom 7224  df-fin 7225  df-card 7940  df-pnf 9242  df-mnf 9243  df-xr 9244  df-ltxr 9245  df-le 9246  df-sub 9417  df-neg 9418  df-nn 10132  df-n0 10389  df-z 10454  df-uz 10669  df-fz 11237  df-hash 11896
  Copyright terms: Public domain W3C validator