Theorem fof 6774

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 626	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6523	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6521	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 294	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ⊆ wss 3904  ran crn 5646   Fn wfn 6512  ⟶wf 6513  –onto→wfo 6515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921  df-f 6521  df-fo 6523

This theorem is referenced by:  fofun  6775  fofn  6776  dffo2  6778  foima  6779  focnvimacdmdm  6786  focofo  6787  resdif  6824  fimacnvinrn  7048  fompt  7095  fconst5  7186  cocan2  7272  foeqcnvco  7280  soisoi  7308  ffoss  7923  focdmex  7933  opco1  8097  opco2  8098  tposf2  8225  smoiso2  8335  mapfoss  8829  ssdomg  8977  fopwdom  9053  unfilem2  9246  fodomfib  9269  fodomfibOLD  9271  fofinf1o  9272  brwdomn0  9514  fowdom  9516  wdomtr  9520  wdomima2g  9531  fodomfi2  10013  wdomfil  10014  alephiso  10051  iunfictbso  10067  cofsmo  10223  isf32lem10  10316  fin1a2lem7  10360  fodomb  10480  iunfo  10493  tskuni  10738  gruima  10757  gruen  10767  axpre-sup  11124  wrdsymb  14552  supcvg  15869  ruclem13  16257  imasval  17524  imasle  17536  imasaddfnlem  17541  imasaddflem  17543  imasvscafn  17550  imasvscaf  17552  imasless  17553  homadm  18056  homacd  18057  dmaf  18065  cdaf  18066  setcepi  18104  imasmnd2  18791  sursubmefmnd  18913  imasgrp2  19080  mhmid  19088  mhmmnd  19089  mhmfmhm  19090  ghmgrp  19091  efgred2  19776  ghmfghm  19853  ghmcyg  19919  gsumval3  19930  gsumzoppg  19967  gsum2dlem2  19994  imasring  20358  znunit  21595  znrrg  21597  cygznlem2a  21599  cygznlem3  21601  cncmp  23432  cnconn  23462  1stcfb  23485  dfac14  23658  qtopval2  23736  qtopuni  23742  qtopid  23745  qtopcld  23753  qtopcn  23754  qtopeu  23756  qtophmeo  23857  elfm3  23990  ovoliunnul  25549  uniiccdif  25620  dchrzrhcl  27286  lgsdchrval  27395  rpvmasumlem  27528  dchrmusum2  27535  dchrvmasumlem3  27540  dchrisum0ff  27548  dchrisum0flblem1  27549  rpvmasum2  27553  dchrisum0re  27554  dchrisum0lem2a  27558  nodense  27733  bdaydmOLD  27820  bdayon  27822  om2noseqlt  28369  om2noseqlt2  28370  om2noseqf1o  28371  noseqrdgfn  28376  bdayn0sf1o  28440  grpocl  30649  grporndm  30659  vafval  30752  smfval  30754  nvgf  30767  vsfval  30782  hhssabloilem  31410  pjhf  31857  elunop  32021  unopf1o  32065  cnvunop  32067  pjinvari  32340  foresf1o  32652  rabfodom  32653  iunrdx  32712  xppreima  32797  gsumpart  33204  imasmhm  33501  imasghm  33502  imasrhm  33503  qtophaus  34094  sigapildsys  34420  carsgclctunlem3  34578  mtyf  35866  poimirlem26  38109  poimirlem27  38110  volsupnfl  38128  cocanfo  38182  exidreslem  38340  rngosn3  38387  rngodm1dm2  38395  founiiun  45721  founiiun0  45732  issalnnd  46883  sge0fodjrnlem  46954  ismeannd  47005  caragenunicl  47062  fcores  47625  fcoresf1lem  47626  fcoresf1  47627  fcoresfo  47629  3f1oss1  47633  fargshiftfo  48012  uptr2  49806