Theorem fof 5615

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 3403	. . 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 5419	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5417	. 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 1369   C_ wss 3323   ran crn 4836   Fn wfn 5408   -->wf 5409   -onto->wfo 5411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337  df-f 5417  df-fo 5419

This theorem is referenced by:  fofun  5616  fofn  5617  dffo2  5619  foima  5620  resdif  5656  fconst5  5930  fconstfv  5935  cocan2  5991  foeqcnvco  5993  soisoi  6014  ffoss  6533  fornex  6541  algrflem  6676  tposf2  6764  smoiso2  6822  mapsn  7246  ssdomg  7347  fopwdom  7411  unfilem2  7569  fodomfib  7583  fofinf1o  7584  brwdomn0  7776  fowdom  7778  wdomtr  7782  wdomima2g  7793  fodomfi2  8222  wdomfil  8223  alephiso  8260  iunfictbso  8276  cofsmo  8430  isf32lem10  8523  fin1a2lem7  8567  fodomb  8685  iunfo  8695  tskuni  8942  gruima  8961  gruen  8971  axpre-sup  9328  supcvg  13310  ruclem13  13516  imasval  14441  imasle  14453  imasaddfnlem  14458  imasaddflem  14460  imasvscafn  14467  imasvscaf  14469  imasless  14470  homadm  14900  homacd  14901  dmaf  14909  cdaf  14910  setcepi  14948  imasmnd2  15450  imasgrp2  15661  efgred2  16241  ghmcyg  16363  gsumval3OLD  16373  gsumval3  16376  gsumzoppg  16430  gsumzoppgOLD  16431  gsum2dlem2  16450  gsum2dOLD  16452  imasrng  16699  znunit  17971  znrrg  17973  cygznlem2a  17975  cygznlem3  17977  cncmp  18970  cnconn  19001  1stcfb  19024  dfac14  19166  qtopval2  19244  qtopuni  19250  qtopid  19253  qtopcld  19261  qtopcn  19262  qtopeu  19264  qtophmeo  19365  elfm3  19498  ovoliunnul  20965  uniiccdif  21033  dchrzrhcl  22559  lgsdchrval  22661  rpvmasumlem  22711  dchrmusum2  22718  dchrvmasumlem3  22723  dchrisum0ff  22731  dchrisum0flblem1  22732  rpvmasum2  22736  dchrisum0re  22737  dchrisum0lem2a  22741  fargshiftfo  23475  grpocl  23638  grporndm  23648  resgrprn  23718  subgores  23742  issubgoi  23748  ghgrplem2  23805  ghgrp  23806  rngosn  23842  rngodm1dm2  23856  rngosn3  23864  vafval  23932  smfval  23934  nvgf  23947  vsfval  23964  pjhf  25062  elunop  25227  unopf1o  25271  cnvunop  25273  pjinvari  25546  iunrdx  25865  fimacnvinrn  25903  xppreima  25915  ghomfo  27261  ghomcl  27262  ghomgsg  27263  ghomf1olem  27264  bdaydm  27770  volsupnfl  28389  cocanfo  28564  exidreslem  28695