Theorem fof 6796

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ⊆ wss 3895  ran crn 5651   Fn wfn 6533  ⟶wf 6534  –onto→wfo 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896  df-f 6542  df-fo 6544

This theorem is used by:  fofun  6797  fofn  6798  dffo2  6800  foima  6801  focnvimacdmdm  6808  focofo  6809  resdif  6846  fimacnvinrn  7071  fompt  7118  fconst5  7212  cocan2  7300  foeqcnvco  7308  soisoi  7336  ffoss  7958  focdmex  7968  opco1  8136  opco2  8137  tposf2  8270  smoiso2  8380  mapfoss  8877  ssdomg  9030  fopwdom  9107  unfilem2  9301  fodomfib  9323  fofinf1o  9324  brwdomn0  9566  fowdom  9568  wdomtr  9572  wdomima2g  9583  fodomfi2  10142  wdomfil  10143  alephiso  10180  iunfictbso  10196  cofsmo  10350  isf32lem10  10443  fin1a2lem7  10487  fodomb  10608  iunfo  10626  tskuni  10871  gruima  10890  gruen  10900  axpre-sup  11257  wrdsymb  14690  supcvg  16030  ruclem13  16415  imasval  17688  imasle  17700  imasaddfnlem  17705  imasaddflem  17707  imasvscafn  17714  imasvscaf  17716  imasless  17717  homadm  18220  homacd  18221  dmaf  18229  cdaf  18230  setcepi  18268  imasmgm2  18868  imasmnd2  18973  sursubmefmnd  19097  imasgrp2  19270  mhmid  19278  mhmmnd  19279  mhmfmhm  19280  ghmgrp  19281  efgred2  19972  ghmfghm  20049  ghmcyg  20115  gsumval3  20126  gsumzoppg  20163  gsum2dlem2  20190  imasring  20565  znunit  21874  znrrg  21876  cygznlem2a  21878  cygznlem3  21880  cncmp  23715  cnconn  23745  1stcfb  23768  dfac14  23942  qtopval2  24020  qtopuni  24026  qtopid  24029  qtopcld  24037  qtopcn  24038  qtopeu  24040  qtophmeo  24141  elfm3  24274  ovoliunnul  25833  uniiccdif  25904  dchrzrhcl  27577  lgsdchrval  27686  rpvmasumlem  27819  dchrmusum2  27826  dchrvmasumlem3  27831  dchrisum0ff  27839  dchrisum0flblem1  27840  rpvmasum2  27844  dchrisum0re  27845  dchrisum0lem2a  27849  nodense  28054  bdaydmOLD  28141  bdayon  28143  om2noseqlt  28690  om2noseqlt2  28691  om2noseqf1o  28692  noseqrdgfn  28697  bdayn0sf1o  28761  grpocl  31107  grporndm  31117  vafval  31210  smfval  31212  nvgf  31225  vsfval  31240  hhssabloilem  31868  pjhf  32315  elunop  32479  unopf1o  32523  cnvunop  32525  pjinvari  32798  foresf1o  33147  rabfodom  33148  iunrdx  33205  xppreima  33286  gsumpart  33670  imasmhm  33961  imasghm  33962  imasrhm  33963  qtophaus  34514  sigapildsys  34841  carsgclctunlem3  34998  werankwe  35791  werankwe2  35792  dfscott3  35797  mtyf  36403  poimirlem26  38657  poimirlem27  38658  volsupnfl  38676  cocanfo  38746  exidreslem  38904  rngosn3  38951  rngodm1dm2  38959  founiiun  46287  founiiun0  46298  issalnnd  47448  sge0fodjrnlem  47519  ismeannd  47570  caragenunicl  47627  fcores  48230  fcoresf1lem  48231  fcoresf1  48232  fcoresfo  48234  3f1oss1  48238  fargshiftfo  48617  uptr2  50430