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

Theorem fofn 5658
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 5656 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffn 5594 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 1  |-  ( F : A -onto-> B  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    Fn wfn 5452   -->wf 5453   -onto->wfo 5455
This theorem is referenced by:  fodmrnu  5664  foun  5696  fo00  5714  cbvfo  6025  foeqcnvco  6030  1stcof  6377  2ndcof  6378  df1st2  6436  df2nd2  6437  1stconst  6438  2ndconst  6439  fsplit  6454  canth  6542  smoiso2  6634  fodomfi  7388  brwdom2  7544  fodomfi2  7946  fpwwe  8526  imasaddfnlem  13758  imasvscafn  13767  imasleval  13771  dmaf  14209  cdaf  14210  imasmnd2  14737  imasgrp2  14938  efgrelexlemb  15387  efgredeu  15389  imasrng  15730  znf1o  16837  zzngim  16838  1stcfb  17513  upxp  17660  uptx  17662  cnmpt1st  17705  cnmpt2nd  17706  qtoptopon  17741  qtopcld  17750  qtopeu  17753  qtoprest  17754  imastopn  17757  qtophmeo  17854  elfm3  17987  uniiccdif  19475  dirith  21228  fargshiftfo  21630  grporn  21805  subgores  21897  vcoprnelem  22062  0vfval  22090  xppreima2  24065  1stpreima  24100  2ndpreima  24101  cnre2csqima  24314  br1steq  25403  br2ndeq  25404  fnbigcup  25751  ovoliunnfl  26260  voliunnfl  26262  volsupnfl  26263  filnetlem4  26424  indlcim  27301
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336  df-f 5461  df-fo 5463
  Copyright terms: Public domain W3C validator