Theorem fof 6735

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3902  ran crn 5617   Fn wfn 6476  ⟶wf 6477  –onto→wfo 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919  df-f 6485  df-fo 6487

This theorem is referenced by:  fofun  6736  fofn  6737  dffo2  6739  foima  6740  focnvimacdmdm  6747  focofo  6748  resdif  6784  fimacnvinrn  7004  fompt  7051  fconst5  7140  cocan2  7226  foeqcnvco  7234  soisoi  7262  ffoss  7878  focdmex  7888  opco1  8053  opco2  8054  tposf2  8180  smoiso2  8289  mapfoss  8776  ssdomg  8922  fopwdom  8998  unfilem2  9190  fodomfib  9213  fodomfibOLD  9215  fofinf1o  9216  brwdomn0  9455  fowdom  9457  wdomtr  9461  wdomima2g  9472  fodomfi2  9948  wdomfil  9949  alephiso  9986  iunfictbso  10002  cofsmo  10157  isf32lem10  10250  fin1a2lem7  10294  fodomb  10414  iunfo  10427  tskuni  10671  gruima  10690  gruen  10700  axpre-sup  11057  wrdsymb  14446  supcvg  15760  ruclem13  16148  imasval  17412  imasle  17424  imasaddfnlem  17429  imasaddflem  17431  imasvscafn  17438  imasvscaf  17440  imasless  17441  homadm  17944  homacd  17945  dmaf  17953  cdaf  17954  setcepi  17992  imasmnd2  18679  sursubmefmnd  18801  imasgrp2  18965  mhmid  18973  mhmmnd  18974  mhmfmhm  18975  ghmgrp  18976  efgred2  19663  ghmfghm  19740  ghmcyg  19806  gsumval3  19817  gsumzoppg  19854  gsum2dlem2  19881  imasring  20246  znunit  21498  znrrg  21500  cygznlem2a  21502  cygznlem3  21504  cncmp  23305  cnconn  23335  1stcfb  23358  dfac14  23531  qtopval2  23609  qtopuni  23615  qtopid  23618  qtopcld  23626  qtopcn  23627  qtopeu  23629  qtophmeo  23730  elfm3  23863  ovoliunnul  25433  uniiccdif  25504  dchrzrhcl  27181  lgsdchrval  27290  rpvmasumlem  27423  dchrmusum2  27430  dchrvmasumlem3  27435  dchrisum0ff  27443  dchrisum0flblem1  27444  rpvmasum2  27448  dchrisum0re  27449  dchrisum0lem2a  27453  nodense  27629  bdaydm  27711  bdayelon  27713  om2noseqlt  28227  om2noseqlt2  28228  om2noseqf1o  28229  noseqrdgfn  28234  bdayn0sf1o  28293  grpocl  30475  grporndm  30485  vafval  30578  smfval  30580  nvgf  30593  vsfval  30608  hhssabloilem  31236  pjhf  31683  elunop  31847  unopf1o  31891  cnvunop  31893  pjinvari  32166  foresf1o  32479  rabfodom  32480  iunrdx  32538  xppreima  32622  gsumpart  33032  imasmhm  33314  imasghm  33315  imasrhm  33316  qtophaus  33844  sigapildsys  34170  carsgclctunlem3  34328  mtyf  35584  poimirlem26  37685  poimirlem27  37686  volsupnfl  37704  cocanfo  37758  exidreslem  37916  rngosn3  37963  rngodm1dm2  37971  founiiun  45215  founiiun0  45226  issalnnd  46382  sge0fodjrnlem  46453  ismeannd  46504  caragenunicl  46561  fcores  47097  fcoresf1lem  47098  fcoresf1  47099  fcoresfo  47101  3f1oss1  47105  fargshiftfo  47472  uptr2  49252