Theorem fof 6697

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 3978	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 617	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6443	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6441	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 292	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ⊆ wss 3888  ran crn 5591   Fn wfn 6432  ⟶wf 6433  –onto→wfo 6435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-f 6441  df-fo 6443

This theorem is referenced by:  fofun  6698  fofn  6699  dffo2  6701  foima  6702  focnvimacdmdm  6709  focofo  6710  resdif  6746  fimacnvinrn  6958  fconst5  7090  cocan2  7173  foeqcnvco  7181  soisoi  7208  ffoss  7797  fornex  7807  opco1  7973  opco2  7974  tposf2  8075  smoiso2  8209  mapfoss  8649  ssdomg  8795  fopwdom  8876  unfilem2  9088  fodomfib  9102  fofinf1o  9103  brwdomn0  9337  fowdom  9339  wdomtr  9343  wdomima2g  9354  fodomfi2  9825  wdomfil  9826  alephiso  9863  iunfictbso  9879  cofsmo  10034  isf32lem10  10127  fin1a2lem7  10171  fodomb  10291  iunfo  10304  tskuni  10548  gruima  10567  gruen  10577  axpre-sup  10934  focdmex  14074  wrdsymb  14254  supcvg  15577  ruclem13  15960  imasval  17231  imasle  17243  imasaddfnlem  17248  imasaddflem  17250  imasvscafn  17257  imasvscaf  17259  imasless  17260  homadm  17764  homacd  17765  dmaf  17773  cdaf  17774  setcepi  17812  imasmnd2  18431  sursubmefmnd  18544  imasgrp2  18699  mhmid  18705  mhmmnd  18706  mhmfmhm  18707  ghmgrp  18708  efgred2  19368  ghmfghm  19441  ghmcyg  19506  gsumval3  19517  gsumzoppg  19554  gsum2dlem2  19581  imasring  19867  znunit  20780  znrrg  20782  cygznlem2a  20784  cygznlem3  20786  cncmp  22552  cnconn  22582  1stcfb  22605  dfac14  22778  qtopval2  22856  qtopuni  22862  qtopid  22865  qtopcld  22873  qtopcn  22874  qtopeu  22876  qtophmeo  22977  elfm3  23110  ovoliunnul  24680  uniiccdif  24751  dchrzrhcl  26402  lgsdchrval  26511  rpvmasumlem  26644  dchrmusum2  26651  dchrvmasumlem3  26656  dchrisum0ff  26664  dchrisum0flblem1  26665  rpvmasum2  26669  dchrisum0re  26670  dchrisum0lem2a  26674  grpocl  28871  grporndm  28881  vafval  28974  smfval  28976  nvgf  28989  vsfval  29004  hhssabloilem  29632  pjhf  30079  elunop  30243  unopf1o  30287  cnvunop  30289  pjinvari  30562  foresf1o  30859  rabfodom  30860  iunrdx  30912  xppreima  30992  gsumpart  31324  qtophaus  31795  sigapildsys  32139  carsgclctunlem3  32296  mtyf  33523  nodense  33904  bdaydm  33978  bdayelon  33980  poimirlem26  35812  poimirlem27  35813  volsupnfl  35831  cocanfo  35885  exidreslem  36044  rngosn3  36091  rngodm1dm2  36099  founiiun  42722  founiiun0  42735  issalnnd  43891  sge0fodjrnlem  43961  ismeannd  44012  caragenunicl  44069  fcores  44572  fcoresf1lem  44573  fcoresf1  44574  fcoresfo  44576  fargshiftfo  44905