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

Theorem fof 5594
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 3344 . . 3  |-  ( ran 
F  =  B  ->  ran  F  C_  B )
21anim2i 553 . 2  |-  ( ( F  Fn  A  /\  ran  F  =  B )  ->  ( F  Fn  A  /\  ran  F  C_  B ) )
3 df-fo 5401 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
4 df-f 5399 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
52, 3, 43imtr4i 258 1  |-  ( F : A -onto-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    C_ wss 3264   ran crn 4820    Fn wfn 5390   -->wf 5391   -onto->wfo 5393
This theorem is referenced by:  fofun  5595  fofn  5596  dffo2  5598  foima  5599  resdif  5637  ffoss  5648  fconst5  5889  fconstfv  5894  fornex  5910  cocan2  5965  foeqcnvco  5967  soisoi  5988  algrflem  6392  tposf2  6440  smoiso2  6568  mapsn  6992  ssdomg  7090  fopwdom  7153  unfilem2  7309  fodomfib  7323  fofinf1o  7324  brwdomn0  7471  fowdom  7473  wdomtr  7477  wdomima2g  7488  fodomfi2  7875  wdomfil  7876  alephiso  7913  iunfictbso  7929  cofsmo  8083  isf32lem10  8176  fin1a2lem7  8220  fodomb  8338  iunfo  8348  tskuni  8592  gruima  8611  gruen  8621  axpre-sup  8978  supcvg  12563  ruclem13  12769  imasval  13665  imasle  13676  imasaddfnlem  13681  imasaddflem  13683  imasvscafn  13690  imasvscaf  13692  imasless  13693  homadm  14123  homacd  14124  dmaf  14132  cdaf  14133  setcepi  14171  imasmnd2  14660  imasgrp2  14861  efgred2  15313  ghmcyg  15433  gsumval3  15442  gsumzoppg  15467  gsum2d  15474  imasrng  15653  znunit  16768  znrrg  16770  cygznlem2a  16772  cygznlem3  16774  cncmp  17378  cnconn  17407  1stcfb  17430  dfac14  17572  qtopval2  17650  qtopuni  17656  qtopid  17659  qtopcld  17667  qtopcn  17668  qtopeu  17670  qtophmeo  17771  elfm3  17904  ovoliunnul  19271  uniiccdif  19338  dchrzrhcl  20897  lgsdchrval  20999  rpvmasumlem  21049  dchrmusum2  21056  dchrvmasumlem3  21061  dchrisum0ff  21069  dchrisum0flblem1  21070  rpvmasum2  21074  dchrisum0re  21075  dchrisum0lem2a  21079  fargshiftfo  21474  grpocl  21637  grporndm  21647  resgrprn  21717  subgores  21741  issubgoi  21747  ghgrplem2  21804  ghgrp  21805  rngosn  21841  rngodm1dm2  21855  rngosn3  21863  vafval  21931  smfval  21933  nvgf  21946  vsfval  21963  pjhf  23059  elunop  23224  unopf1o  23268  cnvunop  23270  pjinvari  23543  iunrdx  23859  fimacnvinrn  23891  xppreima  23902  ghomfo  24882  ghomcl  24883  ghomgsg  24884  ghomf1olem  24885  bdaydm  25357  volsupnfl  25957  cocanfo  26111  exidreslem  26244
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-in 3271  df-ss 3278  df-f 5399  df-fo 5401
  Copyright terms: Public domain W3C validator