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

Theorem fof 5656
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 3402 . . 3  |-  ( ran 
F  =  B  ->  ran  F  C_  B )
21anim2i 554 . 2  |-  ( ( F  Fn  A  /\  ran  F  =  B )  ->  ( F  Fn  A  /\  ran  F  C_  B ) )
3 df-fo 5463 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
4 df-f 5461 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
52, 3, 43imtr4i 259 1  |-  ( F : A -onto-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    C_ wss 3322   ran crn 4882    Fn wfn 5452   -->wf 5453   -onto->wfo 5455
This theorem is referenced by:  fofun  5657  fofn  5658  dffo2  5660  foima  5661  resdif  5699  ffoss  5710  fconst5  5952  fconstfv  5957  fornex  5973  cocan2  6028  foeqcnvco  6030  soisoi  6051  algrflem  6458  tposf2  6506  smoiso2  6634  mapsn  7058  ssdomg  7156  fopwdom  7219  unfilem2  7375  fodomfib  7389  fofinf1o  7390  brwdomn0  7540  fowdom  7542  wdomtr  7546  wdomima2g  7557  fodomfi2  7946  wdomfil  7947  alephiso  7984  iunfictbso  8000  cofsmo  8154  isf32lem10  8247  fin1a2lem7  8291  fodomb  8409  iunfo  8419  tskuni  8663  gruima  8682  gruen  8692  axpre-sup  9049  supcvg  12640  ruclem13  12846  imasval  13742  imasle  13753  imasaddfnlem  13758  imasaddflem  13760  imasvscafn  13767  imasvscaf  13769  imasless  13770  homadm  14200  homacd  14201  dmaf  14209  cdaf  14210  setcepi  14248  imasmnd2  14737  imasgrp2  14938  efgred2  15390  ghmcyg  15510  gsumval3  15519  gsumzoppg  15544  gsum2d  15551  imasrng  15730  znunit  16849  znrrg  16851  cygznlem2a  16853  cygznlem3  16855  cncmp  17460  cnconn  17490  1stcfb  17513  dfac14  17655  qtopval2  17733  qtopuni  17739  qtopid  17742  qtopcld  17750  qtopcn  17751  qtopeu  17753  qtophmeo  17854  elfm3  17987  ovoliunnul  19408  uniiccdif  19475  dchrzrhcl  21034  lgsdchrval  21136  rpvmasumlem  21186  dchrmusum2  21193  dchrvmasumlem3  21198  dchrisum0ff  21206  dchrisum0flblem1  21207  rpvmasum2  21211  dchrisum0re  21212  dchrisum0lem2a  21216  fargshiftfo  21630  grpocl  21793  grporndm  21803  resgrprn  21873  subgores  21897  issubgoi  21903  ghgrplem2  21960  ghgrp  21961  rngosn  21997  rngodm1dm2  22011  rngosn3  22019  vafval  22087  smfval  22089  nvgf  22102  vsfval  22119  pjhf  23215  elunop  23380  unopf1o  23424  cnvunop  23426  pjinvari  23699  iunrdx  24019  fimacnvinrn  24052  xppreima  24064  ghomfo  25107  ghomcl  25108  ghomgsg  25109  ghomf1olem  25110  bdaydm  25638  volsupnfl  26263  cocanfo  26433  exidreslem  26566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336  df-f 5461  df-fo 5463
  Copyright terms: Public domain W3C validator