Theorem fof 5608

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

Step	Hyp	Ref	Expression
1		eqimss 3396	. . 3 |- ( ran F = B -> ran F C_ B )
2	1	anim2i 564	. 2 |- ( ( F Fn A /\ ran F = B ) -> ( F Fn A /\ ran F C_ B ) )
3		df-fo 5412	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5410	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5	2, 3, 4	3imtr4i 266	1 |- ( F : A -onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1362   C_ wss 3316   ran crn 4828   Fn wfn 5401   -->wf 5402   -onto->wfo 5404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330  df-f 5410  df-fo 5412

This theorem is referenced by:  fofun  5609  fofn  5610  dffo2  5612  foima  5613  resdif  5649  fconst5  5922  fconstfv  5927  cocan2  5983  foeqcnvco  5985  soisoi  6006  ffoss  6527  fornex  6535  algrflem  6670  tposf2  6758  smoiso2  6816  mapsn  7242  ssdomg  7343  fopwdom  7407  unfilem2  7565  fodomfib  7579  fofinf1o  7580  brwdomn0  7772  fowdom  7774  wdomtr  7778  wdomima2g  7789  fodomfi2  8218  wdomfil  8219  alephiso  8256  iunfictbso  8272  cofsmo  8426  isf32lem10  8519  fin1a2lem7  8563  fodomb  8681  iunfo  8691  tskuni  8938  gruima  8957  gruen  8967  axpre-sup  9324  supcvg  13301  ruclem13  13507  imasval  14432  imasle  14444  imasaddfnlem  14449  imasaddflem  14451  imasvscafn  14458  imasvscaf  14460  imasless  14461  homadm  14891  homacd  14892  dmaf  14900  cdaf  14901  setcepi  14939  imasmnd2  15441  imasgrp2  15650  efgred2  16230  ghmcyg  16352  gsumval3OLD  16362  gsumval3  16365  gsumzoppg  16416  gsumzoppgOLD  16417  gsum2dlem2  16436  gsum2dOLD  16438  imasrng  16646  znunit  17838  znrrg  17840  cygznlem2a  17842  cygznlem3  17844  cncmp  18837  cnconn  18868  1stcfb  18891  dfac14  19033  qtopval2  19111  qtopuni  19117  qtopid  19120  qtopcld  19128  qtopcn  19129  qtopeu  19131  qtophmeo  19232  elfm3  19365  ovoliunnul  20832  uniiccdif  20900  dchrzrhcl  22469  lgsdchrval  22571  rpvmasumlem  22621  dchrmusum2  22628  dchrvmasumlem3  22633  dchrisum0ff  22641  dchrisum0flblem1  22642  rpvmasum2  22646  dchrisum0re  22647  dchrisum0lem2a  22651  fargshiftfo  23347  grpocl  23510  grporndm  23520  resgrprn  23590  subgores  23614  issubgoi  23620  ghgrplem2  23677  ghgrp  23678  rngosn  23714  rngodm1dm2  23728  rngosn3  23736  vafval  23804  smfval  23806  nvgf  23819  vsfval  23836  pjhf  24934  elunop  25099  unopf1o  25143  cnvunop  25145  pjinvari  25418  iunrdx  25738  fimacnvinrn  25776  xppreima  25788  ghomfo  27157  ghomcl  27158  ghomgsg  27159  ghomf1olem  27160  bdaydm  27666  volsupnfl  28280  cocanfo  28455  exidreslem  28586