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

Theorem fof 5645
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 3392 . . 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 5452 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
4 df-f 5450 . 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 1652    C_ wss 3312   ran crn 4871    Fn wfn 5441   -->wf 5442   -onto->wfo 5444
This theorem is referenced by:  fofun  5646  fofn  5647  dffo2  5649  foima  5650  resdif  5688  ffoss  5699  fconst5  5941  fconstfv  5946  fornex  5962  cocan2  6017  foeqcnvco  6019  soisoi  6040  algrflem  6447  tposf2  6495  smoiso2  6623  mapsn  7047  ssdomg  7145  fopwdom  7208  unfilem2  7364  fodomfib  7378  fofinf1o  7379  brwdomn0  7529  fowdom  7531  wdomtr  7535  wdomima2g  7546  fodomfi2  7933  wdomfil  7934  alephiso  7971  iunfictbso  7987  cofsmo  8141  isf32lem10  8234  fin1a2lem7  8278  fodomb  8396  iunfo  8406  tskuni  8650  gruima  8669  gruen  8679  axpre-sup  9036  supcvg  12627  ruclem13  12833  imasval  13729  imasle  13740  imasaddfnlem  13745  imasaddflem  13747  imasvscafn  13754  imasvscaf  13756  imasless  13757  homadm  14187  homacd  14188  dmaf  14196  cdaf  14197  setcepi  14235  imasmnd2  14724  imasgrp2  14925  efgred2  15377  ghmcyg  15497  gsumval3  15506  gsumzoppg  15531  gsum2d  15538  imasrng  15717  znunit  16836  znrrg  16838  cygznlem2a  16840  cygznlem3  16842  cncmp  17447  cnconn  17477  1stcfb  17500  dfac14  17642  qtopval2  17720  qtopuni  17726  qtopid  17729  qtopcld  17737  qtopcn  17738  qtopeu  17740  qtophmeo  17841  elfm3  17974  ovoliunnul  19395  uniiccdif  19462  dchrzrhcl  21021  lgsdchrval  21123  rpvmasumlem  21173  dchrmusum2  21180  dchrvmasumlem3  21185  dchrisum0ff  21193  dchrisum0flblem1  21194  rpvmasum2  21198  dchrisum0re  21199  dchrisum0lem2a  21203  fargshiftfo  21617  grpocl  21780  grporndm  21790  resgrprn  21860  subgores  21884  issubgoi  21890  ghgrplem2  21947  ghgrp  21948  rngosn  21984  rngodm1dm2  21998  rngosn3  22006  vafval  22074  smfval  22076  nvgf  22089  vsfval  22106  pjhf  23202  elunop  23367  unopf1o  23411  cnvunop  23413  pjinvari  23686  iunrdx  24006  fimacnvinrn  24039  xppreima  24051  ghomfo  25094  ghomcl  25095  ghomgsg  25096  ghomf1olem  25097  bdaydm  25625  volsupnfl  26241  cocanfo  26410  exidreslem  26543
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326  df-f 5450  df-fo 5452
  Copyright terms: Public domain W3C validator