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

Theorem fofn 5779
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 5777 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffn 5713 . 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 5565   -->wf 5566   -onto->wfo 5568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475  df-f 5574  df-fo 5576
This theorem is referenced by:  fodmrnu  5785  foun  5816  fo00  5831  foelrni  5896  cbvfo  6167  foeqcnvco  6178  canth  6229  1stcof  6801  2ndcof  6802  df1st2  6859  df2nd2  6860  1stconst  6861  2ndconst  6862  fsplit  6878  smoiso2  7032  fodomfi  7791  brwdom2  7991  fodomfi2  8432  fpwwe  9013  imasaddfnlem  15020  imasvscafn  15029  imasleval  15033  dmaf  15530  cdaf  15531  imasmnd2  16159  imasgrp2  16387  efgrelexlemb  16970  efgredeu  16972  imasring  17466  znf1o  18766  zzngim  18767  indlcim  19045  1stcfb  20115  upxp  20293  uptx  20295  cnmpt1st  20338  cnmpt2nd  20339  qtoptopon  20374  qtopcld  20383  qtopeu  20386  qtoprest  20387  imastopn  20390  qtophmeo  20487  elfm3  20620  uniiccdif  22156  dirith  23915  fargshiftfo  24843  grporn  25415  subgores  25507  vcoprnelem  25672  0vfval  25700  foresf1o  27605  xppreima2  27712  1stpreimas  27755  1stpreima  27756  2ndpreima  27757  ffsrn  27786  gsummpt2d  28009  qtopt1  28076  qtophaus  28077  circcn  28079  cnre2csqima  28131  sigapildsys  28391  carsgclctunlem3  28531  br1steq  29447  br2ndeq  29448  fnbigcup  29782  ovoliunnfl  30299  voliunnfl  30301  volsupnfl  30302  filnetlem4  30442
  Copyright terms: Public domain W3C validator