Theorem fof 6820

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ⊆ wss 3962  ran crn 5689   Fn wfn 6557  ⟶wf 6558  –onto→wfo 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979  df-f 6566  df-fo 6568

This theorem is referenced by:  fofun  6821  fofn  6822  dffo2  6824  foima  6825  focnvimacdmdm  6832  focofo  6833  resdif  6869  fimacnvinrn  7090  fompt  7137  fconst5  7225  cocan2  7311  foeqcnvco  7319  soisoi  7347  ffoss  7968  focdmex  7978  opco1  8146  opco2  8147  tposf2  8273  smoiso2  8407  mapfoss  8890  ssdomg  9038  fopwdom  9118  unfilem2  9341  fodomfib  9366  fodomfibOLD  9368  fofinf1o  9369  brwdomn0  9606  fowdom  9608  wdomtr  9612  wdomima2g  9623  fodomfi2  10097  wdomfil  10098  alephiso  10135  iunfictbso  10151  cofsmo  10306  isf32lem10  10399  fin1a2lem7  10443  fodomb  10563  iunfo  10576  tskuni  10820  gruima  10839  gruen  10849  axpre-sup  11206  wrdsymb  14576  supcvg  15888  ruclem13  16274  imasval  17557  imasle  17569  imasaddfnlem  17574  imasaddflem  17576  imasvscafn  17583  imasvscaf  17585  imasless  17586  homadm  18093  homacd  18094  dmaf  18102  cdaf  18103  setcepi  18141  imasmnd2  18799  sursubmefmnd  18921  imasgrp2  19085  mhmid  19093  mhmmnd  19094  mhmfmhm  19095  ghmgrp  19096  efgred2  19785  ghmfghm  19862  ghmcyg  19928  gsumval3  19939  gsumzoppg  19976  gsum2dlem2  20003  imasring  20343  znunit  21599  znrrg  21601  cygznlem2a  21603  cygznlem3  21605  cncmp  23415  cnconn  23445  1stcfb  23468  dfac14  23641  qtopval2  23719  qtopuni  23725  qtopid  23728  qtopcld  23736  qtopcn  23737  qtopeu  23739  qtophmeo  23840  elfm3  23973  ovoliunnul  25555  uniiccdif  25626  dchrzrhcl  27303  lgsdchrval  27412  rpvmasumlem  27545  dchrmusum2  27552  dchrvmasumlem3  27557  dchrisum0ff  27565  dchrisum0flblem1  27566  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem2a  27575  nodense  27751  bdaydm  27833  bdayelon  27835  om2noseqlt  28319  om2noseqlt2  28320  om2noseqf1o  28321  noseqrdgfn  28326  grpocl  30528  grporndm  30538  vafval  30631  smfval  30633  nvgf  30646  vsfval  30661  hhssabloilem  31289  pjhf  31736  elunop  31900  unopf1o  31944  cnvunop  31946  pjinvari  32219  foresf1o  32531  rabfodom  32532  iunrdx  32583  xppreima  32661  gsumpart  33042  imasmhm  33361  imasghm  33362  imasrhm  33363  qtophaus  33796  sigapildsys  34142  carsgclctunlem3  34301  mtyf  35536  poimirlem26  37632  poimirlem27  37633  volsupnfl  37651  cocanfo  37705  exidreslem  37863  rngosn3  37910  rngodm1dm2  37918  founiiun  45121  founiiun0  45132  issalnnd  46300  sge0fodjrnlem  46371  ismeannd  46422  caragenunicl  46479  fcores  47016  fcoresf1lem  47017  fcoresf1  47018  fcoresfo  47020  3f1oss1  47024  fargshiftfo  47366