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

Theorem fofn 5469
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 5467 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffn 5405 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 15 1  |-  ( F : A -onto-> B  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    Fn wfn 5266   -->wf 5267   -onto->wfo 5269
This theorem is referenced by:  fodmrnu  5475  foun  5507  fo00  5525  cbvfo  5815  foeqcnvco  5820  1stcof  6163  2ndcof  6164  df1st2  6221  df2nd2  6222  1stconst  6223  2ndconst  6224  fsplit  6239  canth  6310  smoiso2  6402  fodomfi  7151  brwdom2  7303  fodomfi2  7703  fpwwe  8284  imasaddfnlem  13446  imasvscafn  13455  imasleval  13459  dmaf  13897  cdaf  13898  imasmnd2  14425  imasgrp2  14626  efgrelexlemb  15075  efgredeu  15077  imasrng  15418  znf1o  16521  zzngim  16522  1stcfb  17187  upxp  17333  uptx  17335  cnmpt1st  17378  cnmpt2nd  17379  qtoptopon  17411  qtopcld  17420  qtopeu  17423  qtoprest  17424  imastopn  17427  qtophmeo  17524  elfm3  17661  uniiccdif  18949  dirith  20694  grporn  20895  subgores  20987  vcoprnelem  21150  0vfval  21178  xppreima2  23227  cnre2csqima  23310  br1steq  24201  br2ndeq  24202  fnbigcup  24512  ovoliunnfl  25001  prj1b  25182  prj3  25183  imfstnrelc  25184  filnetlem4  26433  indlcim  27413  fargshiftfo  28383
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-f 5275  df-fo 5277
  Copyright terms: Public domain W3C validator