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

Theorem fof 5467
Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
fof  |-  ( F : A -onto-> B  ->  F : A --> B )

Proof of Theorem fof
StepHypRef Expression
1 eqimss 3243 . . 3  |-  ( ran 
F  =  B  ->  ran  F  C_  B )
21anim2i 552 . 2  |-  ( ( F  Fn  A  /\  ran  F  =  B )  ->  ( F  Fn  A  /\  ran  F  C_  B ) )
3 df-fo 5277 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
4 df-f 5275 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
52, 3, 43imtr4i 257 1  |-  ( F : A -onto-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    C_ wss 3165   ran crn 4706    Fn wfn 5266   -->wf 5267   -onto->wfo 5269
This theorem is referenced by:  fofun  5468  fofn  5469  dffo2  5471  foima  5472  resdif  5510  ffoss  5521  fconst5  5747  fconstfv  5750  fornex  5766  cocan2  5818  foeqcnvco  5820  soisoi  5841  algrflem  6240  tposf2  6274  smoiso2  6402  mapsn  6825  ssdomg  6923  fopwdom  6986  unfilem2  7138  fodomfib  7152  fofinf1o  7153  brwdomn0  7299  fowdom  7301  wdomtr  7305  wdomima2g  7316  fodomfi2  7703  wdomfil  7704  alephiso  7741  iunfictbso  7757  cofsmo  7911  isf32lem10  8004  fin1a2lem7  8048  fodomb  8167  iunfo  8177  tskuni  8421  gruima  8440  gruen  8450  axpre-sup  8807  supcvg  12330  ruclem13  12536  imasval  13430  imasle  13441  imasaddfnlem  13446  imasaddflem  13448  imasvscafn  13455  imasvscaf  13457  imasless  13458  homadm  13888  homacd  13889  dmaf  13897  cdaf  13898  setcepi  13936  imasmnd2  14425  imasgrp2  14626  efgred2  15078  ghmcyg  15198  gsumval3  15207  gsumzoppg  15232  gsum2d  15239  imasrng  15418  znunit  16533  znrrg  16535  cygznlem2a  16537  cygznlem3  16539  cncmp  17135  cnconn  17164  1stcfb  17187  dfac14  17328  qtopval2  17403  qtopuni  17409  qtopid  17412  qtopcld  17420  qtopcn  17421  qtopeu  17423  qtophmeo  17524  elfm3  17661  ovoliunnul  18882  uniiccdif  18949  dchrzrhcl  20500  lgsdchrval  20602  rpvmasumlem  20652  dchrmusum2  20659  dchrvmasumlem3  20664  dchrisum0ff  20672  dchrisum0flblem1  20673  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem2a  20682  grpocl  20883  grporndm  20893  resgrprn  20963  subgores  20987  issubgoi  20993  ghgrplem2  21050  ghgrp  21051  rngosn  21087  rngodm1dm2  21101  rngosn3  21109  vafval  21175  smfval  21177  nvgf  21190  vsfval  21207  pjhf  22303  elunop  22468  unopf1o  22512  cnvunop  22514  pjinvari  22787  iunrdx  23177  fimacnvinrn  23214  xppreima  23226  ghomfo  24013  ghomcl  24014  ghomgsg  24015  ghomf1olem  24016  bdaydm  24403  dff1o6f  25195  surjsec2  25223  injsurinj  25252  dmrngrp  25442  ltrcmp  25508  rngodmeqrn  25522  domval  25826  codval  25827  idval  25828  cmpval  25829  prismorcset2  26021  domcatfun  26028  codcatfun  26037  domidmor  26051  codidmor  26053  cmp2morpdom  26067  cmp2morpcod  26068  morexcmp  26070  cocanfo  26477  exidreslem  26670  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