Theorem fof 6740

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3898  ran crn 5620   Fn wfn 6481  ⟶wf 6482  –onto→wfo 6484

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 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915  df-f 6490  df-fo 6492

This theorem is referenced by:  fofun  6741  fofn  6742  dffo2  6744  foima  6745  focnvimacdmdm  6752  focofo  6753  resdif  6789  fimacnvinrn  7010  fompt  7057  fconst5  7146  cocan2  7232  foeqcnvco  7240  soisoi  7268  ffoss  7884  focdmex  7894  opco1  8059  opco2  8060  tposf2  8186  smoiso2  8295  mapfoss  8782  ssdomg  8929  fopwdom  9005  unfilem2  9197  fodomfib  9220  fodomfibOLD  9222  fofinf1o  9223  brwdomn0  9462  fowdom  9464  wdomtr  9468  wdomima2g  9479  fodomfi2  9958  wdomfil  9959  alephiso  9996  iunfictbso  10012  cofsmo  10167  isf32lem10  10260  fin1a2lem7  10304  fodomb  10424  iunfo  10437  tskuni  10681  gruima  10700  gruen  10710  axpre-sup  11067  wrdsymb  14451  supcvg  15765  ruclem13  16153  imasval  17417  imasle  17429  imasaddfnlem  17434  imasaddflem  17436  imasvscafn  17443  imasvscaf  17445  imasless  17446  homadm  17949  homacd  17950  dmaf  17958  cdaf  17959  setcepi  17997  imasmnd2  18684  sursubmefmnd  18806  imasgrp2  18970  mhmid  18978  mhmmnd  18979  mhmfmhm  18980  ghmgrp  18981  efgred2  19667  ghmfghm  19744  ghmcyg  19810  gsumval3  19821  gsumzoppg  19858  gsum2dlem2  19885  imasring  20250  znunit  21502  znrrg  21504  cygznlem2a  21506  cygznlem3  21508  cncmp  23308  cnconn  23338  1stcfb  23361  dfac14  23534  qtopval2  23612  qtopuni  23618  qtopid  23621  qtopcld  23629  qtopcn  23630  qtopeu  23632  qtophmeo  23733  elfm3  23866  ovoliunnul  25436  uniiccdif  25507  dchrzrhcl  27184  lgsdchrval  27293  rpvmasumlem  27426  dchrmusum2  27433  dchrvmasumlem3  27438  dchrisum0ff  27446  dchrisum0flblem1  27447  rpvmasum2  27451  dchrisum0re  27452  dchrisum0lem2a  27456  nodense  27632  bdaydm  27714  bdayelon  27716  om2noseqlt  28230  om2noseqlt2  28231  om2noseqf1o  28232  noseqrdgfn  28237  bdayn0sf1o  28296  grpocl  30482  grporndm  30492  vafval  30585  smfval  30587  nvgf  30600  vsfval  30615  hhssabloilem  31243  pjhf  31690  elunop  31854  unopf1o  31898  cnvunop  31900  pjinvari  32173  foresf1o  32486  rabfodom  32487  iunrdx  32545  xppreima  32629  gsumpart  33044  imasmhm  33326  imasghm  33327  imasrhm  33328  qtophaus  33870  sigapildsys  34196  carsgclctunlem3  34354  mtyf  35617  poimirlem26  37706  poimirlem27  37707  volsupnfl  37725  cocanfo  37779  exidreslem  37937  rngosn3  37984  rngodm1dm2  37992  founiiun  45300  founiiun0  45311  issalnnd  46467  sge0fodjrnlem  46538  ismeannd  46589  caragenunicl  46646  fcores  47191  fcoresf1lem  47192  fcoresf1  47193  fcoresfo  47195  3f1oss1  47199  fargshiftfo  47566  uptr2  49346