Theorem fof 6583

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1531   ⊆ wss 3934  ran crn 5549   Fn wfn 6343  ⟶wf 6344  –onto→wfo 6346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-in 3941  df-ss 3950  df-f 6352  df-fo 6354

This theorem is referenced by:  fofun  6584  fofn  6585  dffo2  6587  foima  6588  resdif  6628  fimacnvinrn  6833  fconst5  6961  cocan2  7040  foeqcnvco  7048  soisoi  7073  ffoss  7639  fornex  7649  algrflem  7811  tposf2  7908  smoiso2  7998  ssdomg  8547  fopwdom  8617  unfilem2  8775  fodomfib  8790  fofinf1o  8791  brwdomn0  9025  fowdom  9027  wdomtr  9031  wdomima2g  9042  fodomfi2  9478  wdomfil  9479  alephiso  9516  iunfictbso  9532  cofsmo  9683  isf32lem10  9776  fin1a2lem7  9820  fodomb  9940  iunfo  9953  tskuni  10197  gruima  10216  gruen  10226  axpre-sup  10583  focdmex  13703  wrdsymb  13885  supcvg  15203  ruclem13  15587  imasval  16776  imasle  16788  imasaddfnlem  16793  imasaddflem  16795  imasvscafn  16802  imasvscaf  16804  imasless  16805  homadm  17292  homacd  17293  dmaf  17301  cdaf  17302  setcepi  17340  imasmnd2  17940  sursubmefmnd  18053  imasgrp2  18206  mhmid  18212  mhmmnd  18213  mhmfmhm  18214  ghmgrp  18215  efgred2  18871  ghmfghm  18943  ghmcyg  19008  gsumval3  19019  gsumzoppg  19056  gsum2dlem2  19083  imasring  19361  znunit  20702  znrrg  20704  cygznlem2a  20706  cygznlem3  20708  cncmp  21992  cnconn  22022  1stcfb  22045  dfac14  22218  qtopval2  22296  qtopuni  22302  qtopid  22305  qtopcld  22313  qtopcn  22314  qtopeu  22316  qtophmeo  22417  elfm3  22550  ovoliunnul  24100  uniiccdif  24171  dchrzrhcl  25813  lgsdchrval  25922  rpvmasumlem  26055  dchrmusum2  26062  dchrvmasumlem3  26067  dchrisum0ff  26075  dchrisum0flblem1  26076  rpvmasum2  26080  dchrisum0re  26081  dchrisum0lem2a  26085  grpocl  28269  grporndm  28279  vafval  28372  smfval  28374  nvgf  28387  vsfval  28402  hhssabloilem  29030  pjhf  29477  elunop  29641  unopf1o  29685  cnvunop  29687  pjinvari  29960  foresf1o  30257  rabfodom  30258  iunrdx  30307  xppreima  30386  qtophaus  31093  sigapildsys  31414  carsgclctunlem3  31571  mtyf  32792  nodense  33189  bdaydm  33237  bdayelon  33239  poimirlem26  34910  poimirlem27  34911  volsupnfl  34929  cocanfo  34985  exidreslem  35147  rngosn3  35194  rngodm1dm2  35202  founiiun  41425  founiiun0  41441  issalnnd  42619  sge0fodjrnlem  42689  ismeannd  42740  caragenunicl  42797  fargshiftfo  43593