Theorem fof 5801

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 3551	. . 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 5600	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5598	. 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 1395   C_ wss 3471   ran crn 5009   Fn wfn 5589   -->wf 5590   -onto->wfo 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3478  df-ss 3485  df-f 5598  df-fo 5600

This theorem is referenced by:  fofun  5802  fofn  5803  dffo2  5805  foima  5806  resdif  5842  fconst5  6130  fconstfvOLD  6135  cocan2  6196  foeqcnvco  6204  soisoi  6225  ffoss  6760  fornex  6768  algrflem  6908  tposf2  6997  smoiso2  7058  mapsn  7479  ssdomg  7580  fopwdom  7644  unfilem2  7803  fodomfib  7818  fofinf1o  7819  brwdomn0  8013  fowdom  8015  wdomtr  8019  wdomima2g  8030  fodomfi2  8458  wdomfil  8459  alephiso  8496  iunfictbso  8512  cofsmo  8666  isf32lem10  8759  fin1a2lem7  8803  fodomb  8921  iunfo  8931  tskuni  9178  gruima  9197  gruen  9207  axpre-sup  9563  supcvg  13678  ruclem13  13986  imasval  14927  imasle  14939  imasaddfnlem  14944  imasaddflem  14946  imasvscafn  14953  imasvscaf  14955  imasless  14956  homadm  15445  homacd  15446  dmaf  15454  cdaf  15455  setcepi  15493  imasmnd2  16083  imasgrp2  16311  mhmid  16317  mhmmnd  16318  mhmfmhm  16319  ghmgrp  16320  efgred2  16897  ghmfghm  16965  ghmcyg  17024  gsumval3OLD  17034  gsumval3  17037  gsumzoppg  17093  gsumzoppgOLD  17094  gsum2dlem2  17124  gsum2dOLD  17126  imasring  17394  znunit  18728  znrrg  18730  cygznlem2a  18732  cygznlem3  18734  cncmp  20018  cnconn  20048  1stcfb  20071  dfac14  20244  qtopval2  20322  qtopuni  20328  qtopid  20331  qtopcld  20339  qtopcn  20340  qtopeu  20342  qtophmeo  20443  elfm3  20576  ovoliunnul  22043  uniiccdif  22112  dchrzrhcl  23645  lgsdchrval  23747  rpvmasumlem  23797  dchrmusum2  23804  dchrvmasumlem3  23809  dchrisum0ff  23817  dchrisum0flblem1  23818  rpvmasum2  23822  dchrisum0re  23823  dchrisum0lem2a  23827  fargshiftfo  24764  grpocl  25328  grporndm  25338  resgrprn  25408  subgores  25432  issubgoi  25438  ghgrplem2OLD  25495  ghgrpOLD  25496  rngosn  25532  rngodm1dm2  25546  rngosn3  25554  vafval  25622  smfval  25624  nvgf  25637  vsfval  25654  pjhf  26752  elunop  26917  unopf1o  26961  cnvunop  26963  pjinvari  27236  foresf1o  27530  rabfodom  27531  iunrdx  27568  fimacnvinrn  27618  xppreima  27630  qtophaus  27992  mtyf  29087  ghomfo  29206  ghomcl  29207  ghomgsg  29208  ghomf1olem  29209  bdaydm  29612  volsupnfl  30221  cocanfo  30370  exidreslem  30501