Theorem fof 5727

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 3515	. . 3 |- ( ran F = B -> ran F C_ B )
2	1	anim2i 569	. 2 |- ( ( F Fn A /\ ran F = B ) -> ( F Fn A /\ ran F C_ B ) )
3		df-fo 5531	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5529	. 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 1370   C_ wss 3435   ran crn 4948   Fn wfn 5520   -->wf 5521   -onto->wfo 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3442  df-ss 3449  df-f 5529  df-fo 5531

This theorem is referenced by:  fofun  5728  fofn  5729  dffo2  5731  foima  5732  resdif  5768  fconst5  6043  fconstfv  6048  cocan2  6104  foeqcnvco  6106  soisoi  6127  ffoss  6647  fornex  6655  algrflem  6790  tposf2  6878  smoiso2  6939  mapsn  7363  ssdomg  7464  fopwdom  7528  unfilem2  7687  fodomfib  7701  fofinf1o  7702  brwdomn0  7894  fowdom  7896  wdomtr  7900  wdomima2g  7911  fodomfi2  8340  wdomfil  8341  alephiso  8378  iunfictbso  8394  cofsmo  8548  isf32lem10  8641  fin1a2lem7  8685  fodomb  8803  iunfo  8813  tskuni  9060  gruima  9079  gruen  9089  axpre-sup  9446  supcvg  13435  ruclem13  13641  imasval  14567  imasle  14579  imasaddfnlem  14584  imasaddflem  14586  imasvscafn  14593  imasvscaf  14595  imasless  14596  homadm  15026  homacd  15027  dmaf  15035  cdaf  15036  setcepi  15074  imasmnd2  15576  imasgrp2  15788  efgred2  16370  ghmcyg  16492  gsumval3OLD  16502  gsumval3  16505  gsumzoppg  16561  gsumzoppgOLD  16562  gsum2dlem2  16583  gsum2dOLD  16585  imasrng  16833  znunit  18120  znrrg  18122  cygznlem2a  18124  cygznlem3  18126  cncmp  19126  cnconn  19157  1stcfb  19180  dfac14  19322  qtopval2  19400  qtopuni  19406  qtopid  19409  qtopcld  19417  qtopcn  19418  qtopeu  19420  qtophmeo  19521  elfm3  19654  ovoliunnul  21121  uniiccdif  21190  dchrzrhcl  22716  lgsdchrval  22818  rpvmasumlem  22868  dchrmusum2  22875  dchrvmasumlem3  22880  dchrisum0ff  22888  dchrisum0flblem1  22889  rpvmasum2  22893  dchrisum0re  22894  dchrisum0lem2a  22898  fargshiftfo  23675  grpocl  23838  grporndm  23848  resgrprn  23918  subgores  23942  issubgoi  23948  ghgrplem2  24005  ghgrp  24006  rngosn  24042  rngodm1dm2  24056  rngosn3  24064  vafval  24132  smfval  24134  nvgf  24147  vsfval  24164  pjhf  25262  elunop  25427  unopf1o  25471  cnvunop  25473  pjinvari  25746  iunrdx  26064  fimacnvinrn  26102  xppreima  26114  ghomfo  27453  ghomcl  27454  ghomgsg  27455  ghomf1olem  27456  bdaydm  27962  volsupnfl  28583  cocanfo  28758  exidreslem  28889