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

Theorem fofn 5622
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 5620 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffn 5558 . 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 5416   -->wf 5417   -onto->wfo 5419
This theorem is referenced by:  fodmrnu  5628  foun  5660  fo00  5678  cbvfo  5989  foeqcnvco  5994  1stcof  6341  2ndcof  6342  df1st2  6400  df2nd2  6401  1stconst  6402  2ndconst  6403  fsplit  6418  canth  6506  smoiso2  6598  fodomfi  7352  brwdom2  7505  fodomfi2  7905  fpwwe  8485  imasaddfnlem  13716  imasvscafn  13725  imasleval  13729  dmaf  14167  cdaf  14168  imasmnd2  14695  imasgrp2  14896  efgrelexlemb  15345  efgredeu  15347  imasrng  15688  znf1o  16795  zzngim  16796  1stcfb  17469  upxp  17616  uptx  17618  cnmpt1st  17661  cnmpt2nd  17662  qtoptopon  17697  qtopcld  17706  qtopeu  17709  qtoprest  17710  imastopn  17713  qtophmeo  17810  elfm3  17943  uniiccdif  19431  dirith  21184  fargshiftfo  21586  grporn  21761  subgores  21853  vcoprnelem  22018  0vfval  22046  xppreima2  24021  1stpreima  24056  2ndpreima  24057  cnre2csqima  24270  br1steq  25352  br2ndeq  25353  fnbigcup  25663  ovoliunnfl  26155  voliunnfl  26157  volsupnfl  26158  filnetlem4  26308  indlcim  27186
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302  df-f 5425  df-fo 5427
  Copyright terms: Public domain W3C validator