Theorem fof 6775

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3917  ran crn 5642   Fn wfn 6509  ⟶wf 6510  –onto→wfo 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934  df-f 6518  df-fo 6520

This theorem is referenced by:  fofun  6776  fofn  6777  dffo2  6779  foima  6780  focnvimacdmdm  6787  focofo  6788  resdif  6824  fimacnvinrn  7046  fompt  7093  fconst5  7183  cocan2  7270  foeqcnvco  7278  soisoi  7306  ffoss  7927  focdmex  7937  opco1  8105  opco2  8106  tposf2  8232  smoiso2  8341  mapfoss  8828  ssdomg  8974  fopwdom  9054  unfilem2  9262  fodomfib  9287  fodomfibOLD  9289  fofinf1o  9290  brwdomn0  9529  fowdom  9531  wdomtr  9535  wdomima2g  9546  fodomfi2  10020  wdomfil  10021  alephiso  10058  iunfictbso  10074  cofsmo  10229  isf32lem10  10322  fin1a2lem7  10366  fodomb  10486  iunfo  10499  tskuni  10743  gruima  10762  gruen  10772  axpre-sup  11129  wrdsymb  14514  supcvg  15829  ruclem13  16217  imasval  17481  imasle  17493  imasaddfnlem  17498  imasaddflem  17500  imasvscafn  17507  imasvscaf  17509  imasless  17510  homadm  18009  homacd  18010  dmaf  18018  cdaf  18019  setcepi  18057  imasmnd2  18708  sursubmefmnd  18830  imasgrp2  18994  mhmid  19002  mhmmnd  19003  mhmfmhm  19004  ghmgrp  19005  efgred2  19690  ghmfghm  19767  ghmcyg  19833  gsumval3  19844  gsumzoppg  19881  gsum2dlem2  19908  imasring  20246  znunit  21480  znrrg  21482  cygznlem2a  21484  cygznlem3  21486  cncmp  23286  cnconn  23316  1stcfb  23339  dfac14  23512  qtopval2  23590  qtopuni  23596  qtopid  23599  qtopcld  23607  qtopcn  23608  qtopeu  23610  qtophmeo  23711  elfm3  23844  ovoliunnul  25415  uniiccdif  25486  dchrzrhcl  27163  lgsdchrval  27272  rpvmasumlem  27405  dchrmusum2  27412  dchrvmasumlem3  27417  dchrisum0ff  27425  dchrisum0flblem1  27426  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lem2a  27435  nodense  27611  bdaydm  27693  bdayelon  27695  om2noseqlt  28200  om2noseqlt2  28201  om2noseqf1o  28202  noseqrdgfn  28207  bdayn0sf1o  28266  grpocl  30436  grporndm  30446  vafval  30539  smfval  30541  nvgf  30554  vsfval  30569  hhssabloilem  31197  pjhf  31644  elunop  31808  unopf1o  31852  cnvunop  31854  pjinvari  32127  foresf1o  32440  rabfodom  32441  iunrdx  32499  xppreima  32576  gsumpart  33004  imasmhm  33332  imasghm  33333  imasrhm  33334  qtophaus  33833  sigapildsys  34159  carsgclctunlem3  34318  mtyf  35546  poimirlem26  37647  poimirlem27  37648  volsupnfl  37666  cocanfo  37720  exidreslem  37878  rngosn3  37925  rngodm1dm2  37933  founiiun  45180  founiiun0  45191  issalnnd  46350  sge0fodjrnlem  46421  ismeannd  46472  caragenunicl  46529  fcores  47072  fcoresf1lem  47073  fcoresf1  47074  fcoresfo  47076  3f1oss1  47080  fargshiftfo  47447  uptr2  49214