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

Theorem fofn 5795
Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)
Assertion
Ref Expression
fofn  |-  ( F : A -onto-> B  ->  F  Fn  A )

Proof of Theorem fofn
StepHypRef Expression
1 fof 5793 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffn 5729 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 1  |-  ( F : A -onto-> B  ->  F  Fn  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    Fn wfn 5581   -->wf 5582   -onto->wfo 5584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-f 5590  df-fo 5592
This theorem is referenced by:  fodmrnu  5801  foun  5832  fo00  5847  cbvfo  6178  foeqcnvco  6189  canth  6240  1stcof  6809  2ndcof  6810  df1st2  6866  df2nd2  6867  1stconst  6868  2ndconst  6869  fsplit  6885  smoiso2  7037  fodomfi  7795  brwdom2  7995  fodomfi2  8437  fpwwe  9020  imasaddfnlem  14779  imasvscafn  14788  imasleval  14792  dmaf  15230  cdaf  15231  imasmnd2  15771  imasgrp2  15985  efgrelexlemb  16564  efgredeu  16566  imasrng  17052  znf1o  18357  zzngim  18358  indlcim  18642  1stcfb  19712  upxp  19859  uptx  19861  cnmpt1st  19904  cnmpt2nd  19905  qtoptopon  19940  qtopcld  19949  qtopeu  19952  qtoprest  19953  imastopn  19956  qtophmeo  20053  elfm3  20186  uniiccdif  21722  dirith  23442  fargshiftfo  24314  grporn  24890  subgores  24982  vcoprnelem  25147  0vfval  25175  xppreima2  27160  1stpreima  27196  2ndpreima  27197  ffsrn  27224  cnre2csqima  27529  qtopt1  27636  qtophaus  27637  circcn  27639  br1steq  28781  br2ndeq  28782  fnbigcup  29128  ovoliunnfl  29633  voliunnfl  29635  volsupnfl  29636  filnetlem4  29802
  Copyright terms: Public domain W3C validator