Theorem fof 6740

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3905  ran crn 5624   Fn wfn 6481  ⟶wf 6482  –onto→wfo 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922  df-f 6490  df-fo 6492

This theorem is referenced by:  fofun  6741  fofn  6742  dffo2  6744  foima  6745  focnvimacdmdm  6752  focofo  6753  resdif  6789  fimacnvinrn  7009  fompt  7056  fconst5  7146  cocan2  7233  foeqcnvco  7241  soisoi  7269  ffoss  7888  focdmex  7898  opco1  8063  opco2  8064  tposf2  8190  smoiso2  8299  mapfoss  8786  ssdomg  8932  fopwdom  9009  unfilem2  9213  fodomfib  9238  fodomfibOLD  9240  fofinf1o  9241  brwdomn0  9480  fowdom  9482  wdomtr  9486  wdomima2g  9497  fodomfi2  9973  wdomfil  9974  alephiso  10011  iunfictbso  10027  cofsmo  10182  isf32lem10  10275  fin1a2lem7  10319  fodomb  10439  iunfo  10452  tskuni  10696  gruima  10715  gruen  10725  axpre-sup  11082  wrdsymb  14467  supcvg  15781  ruclem13  16169  imasval  17433  imasle  17445  imasaddfnlem  17450  imasaddflem  17452  imasvscafn  17459  imasvscaf  17461  imasless  17462  homadm  17965  homacd  17966  dmaf  17974  cdaf  17975  setcepi  18013  imasmnd2  18666  sursubmefmnd  18788  imasgrp2  18952  mhmid  18960  mhmmnd  18961  mhmfmhm  18962  ghmgrp  18963  efgred2  19650  ghmfghm  19727  ghmcyg  19793  gsumval3  19804  gsumzoppg  19841  gsum2dlem2  19868  imasring  20233  znunit  21488  znrrg  21490  cygznlem2a  21492  cygznlem3  21494  cncmp  23295  cnconn  23325  1stcfb  23348  dfac14  23521  qtopval2  23599  qtopuni  23605  qtopid  23608  qtopcld  23616  qtopcn  23617  qtopeu  23619  qtophmeo  23720  elfm3  23853  ovoliunnul  25424  uniiccdif  25495  dchrzrhcl  27172  lgsdchrval  27281  rpvmasumlem  27414  dchrmusum2  27421  dchrvmasumlem3  27426  dchrisum0ff  27434  dchrisum0flblem1  27435  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem2a  27444  nodense  27620  bdaydm  27702  bdayelon  27704  om2noseqlt  28216  om2noseqlt2  28217  om2noseqf1o  28218  noseqrdgfn  28223  bdayn0sf1o  28282  grpocl  30462  grporndm  30472  vafval  30565  smfval  30567  nvgf  30580  vsfval  30595  hhssabloilem  31223  pjhf  31670  elunop  31834  unopf1o  31878  cnvunop  31880  pjinvari  32153  foresf1o  32466  rabfodom  32467  iunrdx  32525  xppreima  32602  gsumpart  33023  imasmhm  33301  imasghm  33302  imasrhm  33303  qtophaus  33802  sigapildsys  34128  carsgclctunlem3  34287  mtyf  35524  poimirlem26  37625  poimirlem27  37626  volsupnfl  37644  cocanfo  37698  exidreslem  37856  rngosn3  37903  rngodm1dm2  37911  founiiun  45157  founiiun0  45168  issalnnd  46327  sge0fodjrnlem  46398  ismeannd  46449  caragenunicl  46506  fcores  47052  fcoresf1lem  47053  fcoresf1  47054  fcoresfo  47056  3f1oss1  47060  fargshiftfo  47427  uptr2  49207