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

Theorem fof 5451
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 3230 . . 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 5261 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
4 df-f 5259 . 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 1623    C_ wss 3152   ran crn 4690    Fn wfn 5250   -->wf 5251   -onto->wfo 5253
This theorem is referenced by:  fofun  5452  fofn  5453  dffo2  5455  foima  5456  resdif  5494  ffoss  5505  fconst5  5731  fconstfv  5734  fornex  5750  cocan2  5802  foeqcnvco  5804  soisoi  5825  algrflem  6224  tposf2  6258  smoiso2  6386  mapsn  6809  ssdomg  6907  fopwdom  6970  unfilem2  7122  fodomfib  7136  fofinf1o  7137  brwdomn0  7283  fowdom  7285  wdomtr  7289  wdomima2g  7300  fodomfi2  7687  wdomfil  7688  alephiso  7725  iunfictbso  7741  cofsmo  7895  isf32lem10  7988  fin1a2lem7  8032  fodomb  8151  iunfo  8161  tskuni  8405  gruima  8424  gruen  8434  axpre-sup  8791  supcvg  12314  ruclem13  12520  imasval  13414  imasle  13425  imasaddfnlem  13430  imasaddflem  13432  imasvscafn  13439  imasvscaf  13441  imasless  13442  homadm  13872  homacd  13873  dmaf  13881  cdaf  13882  setcepi  13920  imasmnd2  14409  imasgrp2  14610  efgred2  15062  ghmcyg  15182  gsumval3  15191  gsumzoppg  15216  gsum2d  15223  imasrng  15402  znunit  16517  znrrg  16519  cygznlem2a  16521  cygznlem3  16523  cncmp  17119  cnconn  17148  1stcfb  17171  dfac14  17312  qtopval2  17387  qtopuni  17393  qtopid  17396  qtopcld  17404  qtopcn  17405  qtopeu  17407  qtophmeo  17508  elfm3  17645  ovoliunnul  18866  uniiccdif  18933  dchrzrhcl  20484  lgsdchrval  20586  rpvmasumlem  20636  dchrmusum2  20643  dchrvmasumlem3  20648  dchrisum0ff  20656  dchrisum0flblem1  20657  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem2a  20666  grpocl  20867  grporndm  20877  resgrprn  20947  subgores  20971  issubgoi  20977  ghgrplem2  21034  ghgrp  21035  rngosn  21071  rngodm1dm2  21085  rngosn3  21093  vafval  21159  smfval  21161  nvgf  21174  vsfval  21191  pjhf  22287  elunop  22452  unopf1o  22496  cnvunop  22498  pjinvari  22771  iunrdx  23161  fimacnvinrn  23199  xppreima  23211  ghomfo  23998  ghomcl  23999  ghomgsg  24000  ghomf1olem  24001  bdaydm  24332  dff1o6f  25092  surjsec2  25120  injsurinj  25149  dmrngrp  25339  ltrcmp  25405  rngodmeqrn  25419  domval  25723  codval  25724  idval  25725  cmpval  25726  prismorcset2  25918  domcatfun  25925  codcatfun  25934  domidmor  25948  codidmor  25950  cmp2morpdom  25964  cmp2morpcod  25965  morexcmp  25967  cocanfo  26374  exidreslem  26567
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-f 5259  df-fo 5261
  Copyright terms: Public domain W3C validator