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

Theorem f1of 5821
Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of

Proof of Theorem f1of
StepHypRef Expression
1 f1of1 5820 . 2
2 f1f 5786 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  -->wf 5589  -1-1->wf1 5590  -1-1-onto->wf1o 5592
This theorem is referenced by:  f1ofn  5822  f1ompt  6053  f1oresrab  6063  fsn  6069  fsnunf  6109  f1ocnvfv1  6182  f1ocnvfv2  6183  f1ocnvdm  6188  fcof1oinvd  6196  fveqf1o  6205  isocnv  6226  isocnv3  6228  isores2  6229  isotr  6232  isofr2  6240  isopolem  6241  isosolem  6243  f1oiso2  6248  weniso  6250  f1ofveu  6291  f1oexrnex  6749  f1oabexg  6759  wemoiso  6785  suppsnop  6932  smoiso  7052  mapsn  7480  ralxpmap  7488  f1oen2g  7552  en1  7602  enfixsn  7646  mapen  7701  ac6sfi  7784  domunfican  7813  fiint  7817  mapfienlem1  7884  mapfienlem2  7885  mapfienlem3  7886  mapfien  7887  supisoex  7953  supiso  7954  ordiso2  7961  ordtypelem10  7973  hartogslem1  7988  unxpwdom2  8035  cantnfle  8111  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1d  8128  cantnflem1  8129  cantnfleOLD  8141  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1dOLD  8151  cantnflem1OLD  8152  mapfienOLD  8159  cnfcomlem  8164  cnfcom  8165  cnfcom2lem  8166  cnfcom2  8167  cnfcom3lem  8168  cnfcom3  8169  cnfcom3clem  8170  cnfcomlemOLD  8172  cnfcomOLD  8173  cnfcom2lemOLD  8174  cnfcom2OLD  8175  cnfcom3lemOLD  8176  cnfcom3OLD  8177  cnfcom3clemOLD  8178  infxpenlem  8412  infxpenc  8416  infxpenc2lem2  8418  infxpencOLD  8421  infxpenc2lem2OLD  8422  fseqenlem1  8426  acndom  8453  acndom2  8456  infpwfien  8464  iunfictbso  8516  infmap2  8619  ackbij2lem2  8641  infpssrlem3  8706  infpssrlem4  8707  fin23lem30  8743  isf32lem6  8759  isf32lem7  8760  isf32lem8  8761  enfin1ai  8785  axcc3  8839  axcclem  8858  ttukeylem7  8916  fpwwe2lem6  9034  fpwwe2lem7  9035  fpwwe2lem9  9037  canthp1lem2  9052  canthp1  9053  pwfseqlem4a  9060  pwfseqlem5  9062  dfle2  11382  axdc4uzlem  12092  seqf1olem1  12146  seqf1olem2  12147  seqf1o  12148  hashkf  12407  hasheqf1oi  12424  hashcl  12428  hashgadd  12445  hashfacen  12503  hashf1lem1  12504  fz1isolem  12510  seqcoll  12512  seqcoll2  12513  snopiswrd  12556  cnrecnv  12998  sumeq2ii  13515  summolem3  13536  summolem2a  13537  fsum  13542  fsumf1o  13545  fsumss  13547  fsumcl2lem  13553  fsumadd  13561  fsummulc2  13599  fsumrelem  13621  ackbijnn  13640  prodeq2ii  13720  prodmolem3  13740  prodmolem2a  13741  fprod  13748  fprodf1o  13753  fprodss  13755  fprodser  13756  fprodcl2lem  13757  fprodmul  13765  fproddiv  13766  fprodn0  13783  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  sadaddlem  14116  sadasslem  14120  sadeq  14122  phimullem  14309  eulerthlem1  14311  eulerthlem2  14312  unbenlem  14426  vdwlem8  14506  0ram  14538  wunndx  14648  xpsaddlem  14972  xpsvsca  14976  xpsle  14978  idfucl  15250  setccatid  15411  setcinv  15417  catcisolem  15433  yonffthlem  15551  gsumpropd2lem  15900  idmhm  15975  mhmf1o  15976  gsumws1  16007  idghm  16282  ghmf1o  16296  symgval  16404  symgbas  16405  elsymgbas  16407  symgbasf  16409  symgbasfi  16411  symg1bas  16421  symggrp  16425  symgid  16426  lactghmga  16429  symgfixf1  16462  f1omvdmvd  16468  f1omvdconj  16471  f1omvdco2  16473  pmtrfconj  16491  symggen  16495  pmtrdifellem1  16501  pmtrdifellem2  16502  psgnunilem1  16518  gsumval3eu  16907  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3  16911  gsumzf1o  16917  gsumzf1oOLD  16920  gsumconst  16954  gsumsub  16974  gsumsubOLD  16975  gsumcom2  17003  dprdfsub  17061  dprdfsubOLD  17068  dprdf1o  17079  dprdsn  17083  ablfaclem2  17137  srngcl  17504  lmhmf1o  17692  fidomndrnglem  17955  psrass1lem  18029  psrnegcl  18049  psrlinv  18050  coe1f2  18248  coe1add  18305  evls1rhmlem  18358  evl1sca  18370  pf1ind  18391  gsumfsum  18484  zntoslem  18595  frgpcyg  18612  islinds2  18848  lindsmm  18863  mat1dimelbas  18973  mat1dimmul  18978  mat1f  18984  mdetleib2  19090  mdetrsca  19105  mdetralt  19110  mdetunilem7  19120  mdetunilem9  19122  ssidcn  19756  hausdiag  20146  hmphdis  20297  indishmph  20299  cmphaushmeo  20301  ordthmeolem  20302  txhmeo  20304  pt1hmeo  20307  qtopf1  20317  ufldom  20463  symgtgp  20600  tsmsf1o  20647  iducn  20786  imasdsf1olem  20876  xpsdsval  20884  imasf1obl  20991  icchmeo  21441  iccpnfcnv  21444  xrhmeo  21446  cnheiborlem  21454  ovolctb  21901  ovoliunlem1  21913  ovoliunlem2  21914  iunmbl2  21967  dyadmbl  22009  vitalilem2  22018  vitalilem3  22019  vitalilem4  22020  vitalilem5  22021  mbfid  22043  dvid  22321  dvexp  22356  dvcnvlem  22377  dvcnv  22378  dvcnvrelem2  22419  dvcnvre  22420  efcvx  22844  reefgim  22845  efif1olem4  22932  eff1olem  22935  logrncl  22955  relogcl  22963  dvrelog  23018  relogcn  23019  logcn  23028  logf1o2  23031  dvlog  23032  dvlog2  23034  advlog  23035  advlogexp  23036  logtayl  23041  logccv  23044  dvcxp1  23116  loglesqrt  23132  asinrebnd  23232  dvatan  23266  efrlim  23299  amgmlem  23319  wilthlem2  23343  wilthlem3  23344  sqff1o  23456  lgsqrlem4  23619  logdivsum  23718  log2sumbnd  23729  isismt  23921  motcl  23926  motco  23927  cnvmot  23928  motgrp  23930  motcgrg  23931  f1otrg  24174  f1otrge  24175  axlowdimlem10  24254  axcontlem5  24271  axcontlem10  24276  umgra1  24326  iseupa  24965  eupatrl  24968  eupa0  24974  eupares  24975  eupap1  24976  eupath2lem3  24979  grposn  25217  ginvsn  25351  dmadjrn  26814  unopnorm  26836  unopadj  26838  unoplin  26839  counop  26840  idcnop  26900  idhmop  26901  unopbd  26934  bracnln  27028  cnvbraval  27029  leopnmid  27057  nmopleid  27058  hmopidmch  27072  hmopidmpj  27073  disjrdx  27450  isoun  27520  fcobij  27548  fcobijfs  27549  abliso  27686  tpr2rico  27894  xrge0iifmhm  27921  xrge0pluscn  27922  rrhre  27999  esumf1o  28061  volmeas  28203  eulerpartgbij  28311  eulerpartlemmf  28314  eulerpartlemgvv  28315  eulerpartlemgf  28318  eulerpartlemgs2  28319  eulerpartlemn  28320  ballotlemsima  28454  lgamcvg2  28597  deranglem  28610  derangsn  28614  derangenlem  28615  subfacp1lem4  28627  subfacp1lem5  28628  subfacp1lem6  28629  cvmfolem  28724  cvmliftlem6  28735  ghomsn  29028  mblfinlem2  30052  dvasin  30103  f1ocan1fv  30217  metf1o  30248  ismtyval  30296  isismty  30297  ismtyima  30299  ismtyhmeolem  30300  ismtybndlem  30302  ismrer1  30334  reheibor  30335  rngoisocnv  30384  mapfzcons  30648  mzpresrename  30683  diophrw  30692  eldioph2  30695  diophren  30747  kelac1  31009  imasgim  31048  lnrfg  31068  stoweidlem27  31809  stoweidlem31  31813  stoweidlem39  31821  fourierdlem20  31909  fourierdlem50  31939  fourierdlem52  31941  fourierdlem54  31943  fourierdlem64  31953  fourierdlem76  31965  fourierdlem102  31991  fourierdlem114  32003  mgmhmf1o  32475  idmgmhm  32476  estrccatid  32638  funcestrcsetclem7  32652  funcestrcsetclem8  32653  funcsetcestrclem7  32667  funcsetcestrclem8  32668  funcringcsetcOLD2lem8  32851  funcringcsetclem8OLD  32874  lflnegl  34801  lautset  35806  islaut  35807  lautcl  35811  lautco  35821  pautsetN  35822  ispautN  35823  ldilco  35840  ltrncoidN  35852  ltrncoval  35869  trlcoabs2N  36448  trlcoat  36449  trlcone  36454  cdlemg47a  36460  cdlemg46  36461  cdlemg47  36462  trljco  36466  tgrpgrplem  36475  tendoidcl  36495  tendo0co2  36514  tendo0pl  36517  cdlemi2  36545  cdlemk2  36558  cdlemk4  36560  cdlemk8  36564  cdlemkid2  36650  cdlemk45  36673  cdlemk53b  36682  cdlemk53  36683  cdlemk55a  36685  erng1r  36721  tendocnv  36748  dvalveclem  36752  dva0g  36754  dvhgrp  36834  dvh0g  36838  dvhopN  36843  cdlemn3  36924  cdlemn8  36931  cdlemn9  36932  dihordlem7b  36942  dihopelvalcpre  36975  dihmeetlem1N  37017  dihglblem5apreN  37018  lcfrlem13  37282  hvmapclN  37491  hvmapcl2  37493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-f1 5598  df-f1o 5600
  Copyright terms: Public domain W3C validator