Theorem fof 6672

Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
fof	⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem fof

Step	Hyp	Ref	Expression
1		eqimss 3973	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 616	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6424	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6422	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 291	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ⊆ wss 3883  ran crn 5581   Fn wfn 6413  ⟶wf 6414  –onto→wfo 6416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422  df-fo 6424

This theorem is referenced by:  fofun  6673  fofn  6674  dffo2  6676  foima  6677  focnvimacdmdm  6684  focofo  6685  resdif  6720  fimacnvinrn  6931  fconst5  7063  cocan2  7144  foeqcnvco  7152  soisoi  7179  ffoss  7762  fornex  7772  opco1  7935  opco2  7936  tposf2  8037  smoiso2  8171  mapfoss  8598  ssdomg  8741  fopwdom  8820  unfilem2  9009  fodomfib  9023  fofinf1o  9024  brwdomn0  9258  fowdom  9260  wdomtr  9264  wdomima2g  9275  fodomfi2  9747  wdomfil  9748  alephiso  9785  iunfictbso  9801  cofsmo  9956  isf32lem10  10049  fin1a2lem7  10093  fodomb  10213  iunfo  10226  tskuni  10470  gruima  10489  gruen  10499  axpre-sup  10856  focdmex  13993  wrdsymb  14173  supcvg  15496  ruclem13  15879  imasval  17139  imasle  17151  imasaddfnlem  17156  imasaddflem  17158  imasvscafn  17165  imasvscaf  17167  imasless  17168  homadm  17671  homacd  17672  dmaf  17680  cdaf  17681  setcepi  17719  imasmnd2  18337  sursubmefmnd  18450  imasgrp2  18605  mhmid  18611  mhmmnd  18612  mhmfmhm  18613  ghmgrp  18614  efgred2  19274  ghmfghm  19347  ghmcyg  19412  gsumval3  19423  gsumzoppg  19460  gsum2dlem2  19487  imasring  19773  znunit  20683  znrrg  20685  cygznlem2a  20687  cygznlem3  20689  cncmp  22451  cnconn  22481  1stcfb  22504  dfac14  22677  qtopval2  22755  qtopuni  22761  qtopid  22764  qtopcld  22772  qtopcn  22773  qtopeu  22775  qtophmeo  22876  elfm3  23009  ovoliunnul  24576  uniiccdif  24647  dchrzrhcl  26298  lgsdchrval  26407  rpvmasumlem  26540  dchrmusum2  26547  dchrvmasumlem3  26552  dchrisum0ff  26560  dchrisum0flblem1  26561  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lem2a  26570  grpocl  28763  grporndm  28773  vafval  28866  smfval  28868  nvgf  28881  vsfval  28896  hhssabloilem  29524  pjhf  29971  elunop  30135  unopf1o  30179  cnvunop  30181  pjinvari  30454  foresf1o  30751  rabfodom  30752  iunrdx  30804  xppreima  30884  gsumpart  31217  qtophaus  31688  sigapildsys  32030  carsgclctunlem3  32187  mtyf  33414  nodense  33822  bdaydm  33896  bdayelon  33898  poimirlem26  35730  poimirlem27  35731  volsupnfl  35749  cocanfo  35803  exidreslem  35962  rngosn3  36009  rngodm1dm2  36017  founiiun  42604  founiiun0  42617  issalnnd  43774  sge0fodjrnlem  43844  ismeannd  43895  caragenunicl  43952  fcores  44448  fcoresf1lem  44449  fcoresf1  44450  fcoresfo  44452  fargshiftfo  44782