Theorem fof 6793

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3902  ran crn 5660   Fn wfn 6532  ⟶wf 6533  –onto→wfo 6535

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 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919  df-f 6541  df-fo 6543

This theorem is used by:  fofun  6794  fofn  6795  dffo2  6797  foima  6798  focnvimacdmdm  6805  focofo  6806  resdif  6843  fimacnvinrn  7068  fompt  7115  fconst5  7209  cocan2  7297  foeqcnvco  7305  soisoi  7333  ffoss  7947  focdmex  7957  opco1  8124  opco2  8125  tposf2  8252  smoiso2  8362  mapfoss  8857  ssdomg  9010  fopwdom  9087  unfilem2  9280  fodomfib  9302  fofinf1o  9303  brwdomn0  9545  fowdom  9547  wdomtr  9551  wdomima2g  9562  fodomfi2  10067  wdomfil  10068  alephiso  10105  iunfictbso  10121  cofsmo  10275  isf32lem10  10368  fin1a2lem7  10412  fodomb  10533  iunfo  10551  tskuni  10796  gruima  10815  gruen  10825  axpre-sup  11182  wrdsymb  14611  supcvg  15949  ruclem13  16336  imasval  17603  imasle  17615  imasaddfnlem  17620  imasaddflem  17622  imasvscafn  17629  imasvscaf  17631  imasless  17632  homadm  18135  homacd  18136  dmaf  18144  cdaf  18145  setcepi  18183  imasmgm2  18782  imasmnd2  18887  sursubmefmnd  19011  imasgrp2  19184  mhmid  19192  mhmmnd  19193  mhmfmhm  19194  ghmgrp  19195  efgred2  19886  ghmfghm  19963  ghmcyg  20029  gsumval3  20040  gsumzoppg  20077  gsum2dlem2  20104  imasring  20477  znunit  21782  znrrg  21784  cygznlem2a  21786  cygznlem3  21788  cncmp  23623  cnconn  23653  1stcfb  23676  dfac14  23850  qtopval2  23928  qtopuni  23934  qtopid  23937  qtopcld  23945  qtopcn  23946  qtopeu  23948  qtophmeo  24049  elfm3  24182  ovoliunnul  25741  uniiccdif  25812  dchrzrhcl  27489  lgsdchrval  27598  rpvmasumlem  27731  dchrmusum2  27738  dchrvmasumlem3  27743  dchrisum0ff  27751  dchrisum0flblem1  27752  rpvmasum2  27756  dchrisum0re  27757  dchrisum0lem2a  27761  nodense  27936  bdaydmOLD  28023  bdayon  28025  om2noseqlt  28572  om2noseqlt2  28573  om2noseqf1o  28574  noseqrdgfn  28579  bdayn0sf1o  28643  grpocl  30989  grporndm  30999  vafval  31092  smfval  31094  nvgf  31107  vsfval  31122  hhssabloilem  31750  pjhf  32197  elunop  32361  unopf1o  32405  cnvunop  32407  pjinvari  32680  foresf1o  32987  rabfodom  32988  iunrdx  33045  xppreima  33126  gsumpart  33511  imasmhm  33802  imasghm  33803  imasrhm  33804  qtophaus  34354  sigapildsys  34681  carsgclctunlem3  34839  dfscott3  35634  mtyf  36139  poimirlem26  38403  poimirlem27  38404  volsupnfl  38422  cocanfo  38477  exidreslem  38635  rngosn3  38682  rngodm1dm2  38690  founiiun  46019  founiiun0  46030  issalnnd  47181  sge0fodjrnlem  47252  ismeannd  47303  caragenunicl  47360  fcores  47963  fcoresf1lem  47964  fcoresf1  47965  fcoresfo  47967  3f1oss1  47971  fargshiftfo  48350  uptr2  50155