Theorem fof 6754

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3903  ran crn 5633   Fn wfn 6495  ⟶wf 6496  –onto→wfo 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920  df-f 6504  df-fo 6506

This theorem is referenced by:  fofun  6755  fofn  6756  dffo2  6758  foima  6759  focnvimacdmdm  6766  focofo  6767  resdif  6803  fimacnvinrn  7025  fompt  7072  fconst5  7162  cocan2  7248  foeqcnvco  7256  soisoi  7284  ffoss  7900  focdmex  7910  opco1  8075  opco2  8076  tposf2  8202  smoiso2  8311  mapfoss  8801  ssdomg  8949  fopwdom  9025  unfilem2  9218  fodomfib  9241  fodomfibOLD  9243  fofinf1o  9244  brwdomn0  9486  fowdom  9488  wdomtr  9492  wdomima2g  9503  fodomfi2  9982  wdomfil  9983  alephiso  10020  iunfictbso  10036  cofsmo  10191  isf32lem10  10284  fin1a2lem7  10328  fodomb  10448  iunfo  10461  tskuni  10706  gruima  10725  gruen  10735  axpre-sup  11092  wrdsymb  14477  supcvg  15791  ruclem13  16179  imasval  17444  imasle  17456  imasaddfnlem  17461  imasaddflem  17463  imasvscafn  17470  imasvscaf  17472  imasless  17473  homadm  17976  homacd  17977  dmaf  17985  cdaf  17986  setcepi  18024  imasmnd2  18711  sursubmefmnd  18833  imasgrp2  18997  mhmid  19005  mhmmnd  19006  mhmfmhm  19007  ghmgrp  19008  efgred2  19694  ghmfghm  19771  ghmcyg  19837  gsumval3  19848  gsumzoppg  19885  gsum2dlem2  19912  imasring  20278  znunit  21530  znrrg  21532  cygznlem2a  21534  cygznlem3  21536  cncmp  23348  cnconn  23378  1stcfb  23401  dfac14  23574  qtopval2  23652  qtopuni  23658  qtopid  23661  qtopcld  23669  qtopcn  23670  qtopeu  23672  qtophmeo  23773  elfm3  23906  ovoliunnul  25476  uniiccdif  25547  dchrzrhcl  27224  lgsdchrval  27333  rpvmasumlem  27466  dchrmusum2  27473  dchrvmasumlem3  27478  dchrisum0ff  27486  dchrisum0flblem1  27487  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lem2a  27496  nodense  27672  bdaydm  27758  bdayon  27760  om2noseqlt  28307  om2noseqlt2  28308  om2noseqf1o  28309  noseqrdgfn  28314  bdayn0sf1o  28378  grpocl  30587  grporndm  30597  vafval  30690  smfval  30692  nvgf  30705  vsfval  30720  hhssabloilem  31348  pjhf  31795  elunop  31959  unopf1o  32003  cnvunop  32005  pjinvari  32278  foresf1o  32590  rabfodom  32591  iunrdx  32649  xppreima  32734  gsumpart  33156  imasmhm  33446  imasghm  33447  imasrhm  33448  qtophaus  34013  sigapildsys  34339  carsgclctunlem3  34497  mtyf  35765  poimirlem26  37891  poimirlem27  37892  volsupnfl  37910  cocanfo  37964  exidreslem  38122  rngosn3  38169  rngodm1dm2  38177  founiiun  45532  founiiun0  45543  issalnnd  46697  sge0fodjrnlem  46768  ismeannd  46819  caragenunicl  46876  fcores  47421  fcoresf1lem  47422  fcoresf1  47423  fcoresfo  47425  3f1oss1  47429  fargshiftfo  47796  uptr2  49574