Theorem fof 6799

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 3998	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 629	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6549	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6547	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 295	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3908  ran crn 5667   Fn wfn 6538  ⟶wf 6539  –onto→wfo 6541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925  df-f 6547  df-fo 6549

This theorem is used by:  fofun  6800  fofn  6801  dffo2  6803  foima  6804  focnvimacdmdm  6811  focofo  6812  resdif  6849  fimacnvinrn  7073  fompt  7120  fconst5  7211  cocan2  7301  foeqcnvco  7309  soisoi  7337  ffoss  7952  focdmex  7962  opco1  8127  opco2  8128  tposf2  8255  smoiso2  8365  mapfoss  8858  ssdomg  9006  fopwdom  9083  unfilem2  9276  fodomfib  9298  fofinf1o  9299  brwdomn0  9541  fowdom  9543  wdomtr  9547  wdomima2g  9558  fodomfi2  10063  wdomfil  10064  alephiso  10101  iunfictbso  10117  cofsmo  10271  isf32lem10  10364  fin1a2lem7  10408  fodomb  10528  iunfo  10541  tskuni  10786  gruima  10805  gruen  10815  axpre-sup  11172  wrdsymb  14599  supcvg  15936  ruclem13  16323  imasval  17590  imasle  17602  imasaddfnlem  17607  imasaddflem  17609  imasvscafn  17616  imasvscaf  17618  imasless  17619  homadm  18122  homacd  18123  dmaf  18131  cdaf  18132  setcepi  18170  imasmnd2  18863  sursubmefmnd  18986  imasgrp2  19152  mhmid  19160  mhmmnd  19161  mhmfmhm  19162  ghmgrp  19163  efgred2  19854  ghmfghm  19931  ghmcyg  19997  gsumval3  20008  gsumzoppg  20045  gsum2dlem2  20072  imasring  20445  znunit  21750  znrrg  21752  cygznlem2a  21754  cygznlem3  21756  cncmp  23586  cnconn  23616  1stcfb  23639  dfac14  23812  qtopval2  23890  qtopuni  23896  qtopid  23899  qtopcld  23907  qtopcn  23908  qtopeu  23910  qtophmeo  24011  elfm3  24144  ovoliunnul  25703  uniiccdif  25774  dchrzrhcl  27446  lgsdchrval  27555  rpvmasumlem  27688  dchrmusum2  27695  dchrvmasumlem3  27700  dchrisum0ff  27708  dchrisum0flblem1  27709  rpvmasum2  27713  dchrisum0re  27714  dchrisum0lem2a  27718  nodense  27893  bdaydmOLD  27980  bdayon  27982  om2noseqlt  28529  om2noseqlt2  28530  om2noseqf1o  28531  noseqrdgfn  28536  bdayn0sf1o  28600  grpocl  30889  grporndm  30899  vafval  30992  smfval  30994  nvgf  31007  vsfval  31022  hhssabloilem  31650  pjhf  32097  elunop  32261  unopf1o  32305  cnvunop  32307  pjinvari  32580  foresf1o  32887  rabfodom  32888  iunrdx  32945  xppreima  33027  gsumpart  33414  imasmhm  33705  imasghm  33706  imasrhm  33707  qtophaus  34257  sigapildsys  34584  carsgclctunlem3  34742  dfscott3  35537  mtyf  36065  poimirlem26  38338  poimirlem27  38339  volsupnfl  38357  cocanfo  38411  exidreslem  38569  rngosn3  38616  rngodm1dm2  38624  founiiun  45938  founiiun0  45949  issalnnd  47100  sge0fodjrnlem  47171  ismeannd  47222  caragenunicl  47279  fcores  47845  fcoresf1lem  47846  fcoresf1  47847  fcoresfo  47849  3f1oss1  47853  fargshiftfo  48232  uptr2  50040