Theorem fof 5793

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 3484	. . 3 |- ( ran F = B -> ran F C_ B )
2	1	anim2i 573	. 2 |- ( ( F Fn A /\ ran F = B ) -> ( F Fn A /\ ran F C_ B ) )
3		df-fo 5588	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5586	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5	2, 3, 4	3imtr4i 270	1 |- ( F : A -onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1444   C_ wss 3404   ran crn 4835   Fn wfn 5577   -->wf 5578   -onto->wfo 5580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418  df-f 5586  df-fo 5588

This theorem is referenced by:  fofun  5794  fofn  5795  dffo2  5797  foima  5798  resdif  5834  fconst5  6122  fconstfvOLD  6127  cocan2  6190  foeqcnvco  6198  soisoi  6219  ffoss  6754  fornex  6762  algrflem  6905  tposf2  6997  smoiso2  7088  mapsn  7513  ssdomg  7615  fopwdom  7680  unfilem2  7836  fodomfib  7851  fofinf1o  7852  brwdomn0  8084  fowdom  8086  wdomtr  8090  wdomima2g  8101  fodomfi2  8491  wdomfil  8492  alephiso  8529  iunfictbso  8545  cofsmo  8699  isf32lem10  8792  fin1a2lem7  8836  fodomb  8954  iunfo  8964  tskuni  9208  gruima  9227  gruen  9237  axpre-sup  9593  supcvg  13914  ruclem13  14294  imasval  15411  imasvalOLD  15412  imasle  15424  imasaddfnlem  15434  imasaddflem  15436  imasvscafn  15443  imasvscaf  15445  imasless  15446  homadm  15935  homacd  15936  dmaf  15944  cdaf  15945  setcepi  15983  imasmnd2  16573  imasgrp2  16801  mhmid  16807  mhmmnd  16808  mhmfmhm  16809  ghmgrp  16810  efgred2  17403  ghmfghm  17471  ghmcyg  17530  gsumval3  17541  gsumzoppg  17577  gsum2dlem2  17603  imasring  17847  znunit  19134  znrrg  19136  cygznlem2a  19138  cygznlem3  19140  cncmp  20407  cnconn  20437  1stcfb  20460  dfac14  20633  qtopval2  20711  qtopuni  20717  qtopid  20720  qtopcld  20728  qtopcn  20729  qtopeu  20731  qtophmeo  20832  elfm3  20965  ovoliunnul  22460  uniiccdif  22535  dchrzrhcl  24173  lgsdchrval  24275  rpvmasumlem  24325  dchrmusum2  24332  dchrvmasumlem3  24337  dchrisum0ff  24345  dchrisum0flblem1  24346  rpvmasum2  24350  dchrisum0re  24351  dchrisum0lem2a  24355  fargshiftfo  25366  grpocl  25928  grporndm  25938  resgrprn  26008  subgores  26032  issubgoi  26038  ghgrplem2OLD  26095  ghgrpOLD  26096  rngosn  26132  rngodm1dm2  26146  rngosn3  26154  vafval  26222  smfval  26224  nvgf  26237  vsfval  26254  pjhf  27361  elunop  27525  unopf1o  27569  cnvunop  27571  pjinvari  27844  foresf1o  28139  rabfodom  28140  iunrdx  28179  fimacnvinrn  28235  xppreima  28248  qtophaus  28663  sigapildsys  28984  carsgclctunlem3  29152  mtyf  30190  ghomfo  30309  ghomcl  30310  ghomgsg  30311  ghomf1olem  30312  bdaydm  30567  poimirlem26  31966  poimirlem27  31967  volsupnfl  31985  cocanfo  32044  exidreslem  32175  founiiun  37446  founiiun0  37465  mapsnd  37476  sge0fodjrnlem  38258  ismeannd  38305  caragenunicl  38345