Theorem fof 6820

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3951  ran crn 5686   Fn wfn 6556  ⟶wf 6557  –onto→wfo 6559

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-f 6565  df-fo 6567

This theorem is referenced by:  fofun  6821  fofn  6822  dffo2  6824  foima  6825  focnvimacdmdm  6832  focofo  6833  resdif  6869  fimacnvinrn  7091  fompt  7138  fconst5  7226  cocan2  7312  foeqcnvco  7320  soisoi  7348  ffoss  7970  focdmex  7980  opco1  8148  opco2  8149  tposf2  8275  smoiso2  8409  mapfoss  8892  ssdomg  9040  fopwdom  9120  unfilem2  9344  fodomfib  9369  fodomfibOLD  9371  fofinf1o  9372  brwdomn0  9609  fowdom  9611  wdomtr  9615  wdomima2g  9626  fodomfi2  10100  wdomfil  10101  alephiso  10138  iunfictbso  10154  cofsmo  10309  isf32lem10  10402  fin1a2lem7  10446  fodomb  10566  iunfo  10579  tskuni  10823  gruima  10842  gruen  10852  axpre-sup  11209  wrdsymb  14580  supcvg  15892  ruclem13  16278  imasval  17556  imasle  17568  imasaddfnlem  17573  imasaddflem  17575  imasvscafn  17582  imasvscaf  17584  imasless  17585  homadm  18085  homacd  18086  dmaf  18094  cdaf  18095  setcepi  18133  imasmnd2  18787  sursubmefmnd  18909  imasgrp2  19073  mhmid  19081  mhmmnd  19082  mhmfmhm  19083  ghmgrp  19084  efgred2  19771  ghmfghm  19848  ghmcyg  19914  gsumval3  19925  gsumzoppg  19962  gsum2dlem2  19989  imasring  20327  znunit  21582  znrrg  21584  cygznlem2a  21586  cygznlem3  21588  cncmp  23400  cnconn  23430  1stcfb  23453  dfac14  23626  qtopval2  23704  qtopuni  23710  qtopid  23713  qtopcld  23721  qtopcn  23722  qtopeu  23724  qtophmeo  23825  elfm3  23958  ovoliunnul  25542  uniiccdif  25613  dchrzrhcl  27289  lgsdchrval  27398  rpvmasumlem  27531  dchrmusum2  27538  dchrvmasumlem3  27543  dchrisum0ff  27551  dchrisum0flblem1  27552  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lem2a  27561  nodense  27737  bdaydm  27819  bdayelon  27821  om2noseqlt  28305  om2noseqlt2  28306  om2noseqf1o  28307  noseqrdgfn  28312  grpocl  30519  grporndm  30529  vafval  30622  smfval  30624  nvgf  30637  vsfval  30652  hhssabloilem  31280  pjhf  31727  elunop  31891  unopf1o  31935  cnvunop  31937  pjinvari  32210  foresf1o  32523  rabfodom  32524  iunrdx  32576  xppreima  32655  gsumpart  33060  imasmhm  33382  imasghm  33383  imasrhm  33384  qtophaus  33835  sigapildsys  34163  carsgclctunlem3  34322  mtyf  35557  poimirlem26  37653  poimirlem27  37654  volsupnfl  37672  cocanfo  37726  exidreslem  37884  rngosn3  37931  rngodm1dm2  37939  founiiun  45184  founiiun0  45195  issalnnd  46360  sge0fodjrnlem  46431  ismeannd  46482  caragenunicl  46539  fcores  47079  fcoresf1lem  47080  fcoresf1  47081  fcoresfo  47083  3f1oss1  47087  fargshiftfo  47429