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

Theorem fofn 5809
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 5807 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffn 5743 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 17 1  |-  ( F : A -onto-> B  ->  F  Fn  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    Fn wfn 5593   -->wf 5594   -onto->wfo 5596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450  df-f 5602  df-fo 5604
This theorem is referenced by:  fodmrnu  5815  foun  5846  fo00  5861  foelrni  5926  cbvfo  6199  foeqcnvco  6210  canth  6261  1stcof  6832  2ndcof  6833  df1st2  6890  df2nd2  6891  1stconst  6892  2ndconst  6893  fsplit  6909  smoiso2  7093  fodomfi  7853  brwdom2  8091  fodomfi2  8492  fpwwe  9072  imasaddfnlem  15422  imasvscafn  15431  imasleval  15435  dmaf  15932  cdaf  15933  imasmnd2  16561  imasgrp2  16789  efgrelexlemb  17388  efgredeu  17390  imasring  17835  znf1o  19109  zzngim  19110  indlcim  19385  1stcfb  20447  upxp  20625  uptx  20627  cnmpt1st  20670  cnmpt2nd  20671  qtoptopon  20706  qtopcld  20715  qtopeu  20718  qtoprest  20719  imastopn  20722  qtophmeo  20819  elfm3  20952  uniiccdif  22522  dirith  24354  fargshiftfo  25352  grporn  25926  subgores  26018  vcoprnelem  26183  0vfval  26211  foresf1o  28126  xppreima2  28239  1stpreimas  28276  1stpreima  28277  2ndpreima  28278  ffsrn  28308  gsummpt2d  28539  qtopt1  28658  qtophaus  28659  circcn  28661  cnre2csqima  28713  sigapildsys  28980  carsgclctunlem3  29148  br1steq  30409  br2ndeq  30410  fnbigcup  30661  filnetlem4  31030  ovoliunnfl  31896  voliunnfl  31898  volsupnfl  31899  ssnnf1octb  37320  nnfoctbdj  38073
  Copyright terms: Public domain W3C validator