Theorem fof 6782

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ⊆ wss 3907  ran crn 5653   Fn wfn 6520  ⟶wf 6521  –onto→wfo 6523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924  df-f 6529  df-fo 6531

This theorem is referenced by:  fofun  6783  fofn  6784  dffo2  6786  foima  6787  focnvimacdmdm  6794  focofo  6795  resdif  6832  fimacnvinrn  7056  fompt  7103  fconst5  7194  cocan2  7280  foeqcnvco  7288  soisoi  7316  ffoss  7931  focdmex  7941  opco1  8106  opco2  8107  tposf2  8234  smoiso2  8344  mapfoss  8837  ssdomg  8985  fopwdom  9061  unfilem2  9254  fodomfib  9276  fofinf1o  9277  brwdomn0  9519  fowdom  9521  wdomtr  9525  wdomima2g  9536  fodomfi2  10032  wdomfil  10033  alephiso  10070  iunfictbso  10086  cofsmo  10241  isf32lem10  10334  fin1a2lem7  10378  fodomb  10498  iunfo  10511  tskuni  10756  gruima  10775  gruen  10785  axpre-sup  11142  wrdsymb  14569  supcvg  15900  ruclem13  16288  imasval  17555  imasle  17567  imasaddfnlem  17572  imasaddflem  17574  imasvscafn  17581  imasvscaf  17583  imasless  17584  homadm  18087  homacd  18088  dmaf  18096  cdaf  18097  setcepi  18135  imasmnd2  18822  sursubmefmnd  18945  imasgrp2  19112  mhmid  19120  mhmmnd  19121  mhmfmhm  19122  ghmgrp  19123  efgred2  19814  ghmfghm  19891  ghmcyg  19957  gsumval3  19968  gsumzoppg  20005  gsum2dlem2  20032  imasring  20403  znunit  21673  znrrg  21675  cygznlem2a  21677  cygznlem3  21679  cncmp  23510  cnconn  23540  1stcfb  23563  dfac14  23736  qtopval2  23814  qtopuni  23820  qtopid  23823  qtopcld  23831  qtopcn  23832  qtopeu  23834  qtophmeo  23935  elfm3  24068  ovoliunnul  25627  uniiccdif  25698  dchrzrhcl  27367  lgsdchrval  27476  rpvmasumlem  27609  dchrmusum2  27616  dchrvmasumlem3  27621  dchrisum0ff  27629  dchrisum0flblem1  27630  rpvmasum2  27634  dchrisum0re  27635  dchrisum0lem2a  27639  nodense  27814  bdaydmOLD  27901  bdayon  27903  om2noseqlt  28450  om2noseqlt2  28451  om2noseqf1o  28452  noseqrdgfn  28457  bdayn0sf1o  28521  grpocl  30761  grporndm  30771  vafval  30864  smfval  30866  nvgf  30879  vsfval  30894  hhssabloilem  31522  pjhf  31969  elunop  32133  unopf1o  32177  cnvunop  32179  pjinvari  32452  foresf1o  32760  rabfodom  32761  iunrdx  32818  xppreima  32902  gsumpart  33296  imasmhm  33589  imasghm  33590  imasrhm  33591  qtophaus  34143  sigapildsys  34469  carsgclctunlem3  34627  mtyf  35915  poimirlem26  38157  poimirlem27  38158  volsupnfl  38176  cocanfo  38230  exidreslem  38388  rngosn3  38435  rngodm1dm2  38443  founiiun  45755  founiiun0  45766  issalnnd  46917  sge0fodjrnlem  46988  ismeannd  47039  caragenunicl  47096  fcores  47659  fcoresf1lem  47660  fcoresf1  47661  fcoresfo  47663  3f1oss1  47667  fargshiftfo  48046  uptr2  49850