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

Theorem fofn 5723
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 5721 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffn 5660 . 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 5514   -->wf 5515   -onto->wfo 5517
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 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3436  df-ss 3443  df-f 5523  df-fo 5525
This theorem is referenced by:  fodmrnu  5729  foun  5760  fo00  5775  cbvfo  6095  foeqcnvco  6100  canth  6151  1stcof  6707  2ndcof  6708  df1st2  6762  df2nd2  6763  1stconst  6764  2ndconst  6765  fsplit  6780  smoiso2  6933  fodomfi  7694  brwdom2  7892  fodomfi2  8334  fpwwe  8917  imasaddfnlem  14577  imasvscafn  14586  imasleval  14590  dmaf  15028  cdaf  15029  imasmnd2  15569  imasgrp2  15781  efgrelexlemb  16360  efgredeu  16362  imasrng  16826  znf1o  18102  zzngim  18103  indlcim  18387  1stcfb  19174  upxp  19321  uptx  19323  cnmpt1st  19366  cnmpt2nd  19367  qtoptopon  19402  qtopcld  19411  qtopeu  19414  qtoprest  19415  imastopn  19418  qtophmeo  19515  elfm3  19648  uniiccdif  21184  dirith  22904  fargshiftfo  23669  grporn  23844  subgores  23936  vcoprnelem  24101  0vfval  24129  xppreima2  26109  1stpreima  26145  2ndpreima  26146  ffsrn  26173  cnre2csqima  26479  br1steq  27722  br2ndeq  27723  fnbigcup  28069  ovoliunnfl  28574  voliunnfl  28576  volsupnfl  28577  filnetlem4  28743
  Copyright terms: Public domain W3C validator