Theorem fof 6789

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3926  ran crn 5655   Fn wfn 6525  ⟶wf 6526  –onto→wfo 6528

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943  df-f 6534  df-fo 6536

This theorem is referenced by:  fofun  6790  fofn  6791  dffo2  6793  foima  6794  focnvimacdmdm  6801  focofo  6802  resdif  6838  fimacnvinrn  7060  fompt  7107  fconst5  7197  cocan2  7284  foeqcnvco  7292  soisoi  7320  ffoss  7942  focdmex  7952  opco1  8120  opco2  8121  tposf2  8247  smoiso2  8381  mapfoss  8864  ssdomg  9012  fopwdom  9092  unfilem2  9314  fodomfib  9339  fodomfibOLD  9341  fofinf1o  9342  brwdomn0  9581  fowdom  9583  wdomtr  9587  wdomima2g  9598  fodomfi2  10072  wdomfil  10073  alephiso  10110  iunfictbso  10126  cofsmo  10281  isf32lem10  10374  fin1a2lem7  10418  fodomb  10538  iunfo  10551  tskuni  10795  gruima  10814  gruen  10824  axpre-sup  11181  wrdsymb  14558  supcvg  15870  ruclem13  16258  imasval  17523  imasle  17535  imasaddfnlem  17540  imasaddflem  17542  imasvscafn  17549  imasvscaf  17551  imasless  17552  homadm  18051  homacd  18052  dmaf  18060  cdaf  18061  setcepi  18099  imasmnd2  18750  sursubmefmnd  18872  imasgrp2  19036  mhmid  19044  mhmmnd  19045  mhmfmhm  19046  ghmgrp  19047  efgred2  19732  ghmfghm  19809  ghmcyg  19875  gsumval3  19886  gsumzoppg  19923  gsum2dlem2  19950  imasring  20288  znunit  21522  znrrg  21524  cygznlem2a  21526  cygznlem3  21528  cncmp  23328  cnconn  23358  1stcfb  23381  dfac14  23554  qtopval2  23632  qtopuni  23638  qtopid  23641  qtopcld  23649  qtopcn  23650  qtopeu  23652  qtophmeo  23753  elfm3  23886  ovoliunnul  25458  uniiccdif  25529  dchrzrhcl  27206  lgsdchrval  27315  rpvmasumlem  27448  dchrmusum2  27455  dchrvmasumlem3  27460  dchrisum0ff  27468  dchrisum0flblem1  27469  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lem2a  27478  nodense  27654  bdaydm  27736  bdayelon  27738  om2noseqlt  28222  om2noseqlt2  28223  om2noseqf1o  28224  noseqrdgfn  28229  grpocl  30427  grporndm  30437  vafval  30530  smfval  30532  nvgf  30545  vsfval  30560  hhssabloilem  31188  pjhf  31635  elunop  31799  unopf1o  31843  cnvunop  31845  pjinvari  32118  foresf1o  32431  rabfodom  32432  iunrdx  32490  xppreima  32569  gsumpart  32997  imasmhm  33315  imasghm  33316  imasrhm  33317  qtophaus  33813  sigapildsys  34139  carsgclctunlem3  34298  mtyf  35520  poimirlem26  37616  poimirlem27  37617  volsupnfl  37635  cocanfo  37689  exidreslem  37847  rngosn3  37894  rngodm1dm2  37902  founiiun  45151  founiiun0  45162  issalnnd  46322  sge0fodjrnlem  46393  ismeannd  46444  caragenunicl  46501  fcores  47044  fcoresf1lem  47045  fcoresf1  47046  fcoresfo  47048  3f1oss1  47052  fargshiftfo  47404