Theorem fof 6611

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ⊆ wss 3853  ran crn 5537   Fn wfn 6353  ⟶wf 6354  –onto→wfo 6356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-f 6362  df-fo 6364

This theorem is referenced by:  fofun  6612  fofn  6613  dffo2  6615  foima  6616  focnvimacdmdm  6623  focofo  6624  resdif  6659  fimacnvinrn  6870  fconst5  6999  cocan2  7080  foeqcnvco  7088  soisoi  7115  ffoss  7697  fornex  7707  algrflem  7870  tposf2  7970  smoiso2  8084  mapfoss  8511  ssdomg  8652  fopwdom  8731  unfilem2  8914  fodomfib  8928  fofinf1o  8929  brwdomn0  9163  fowdom  9165  wdomtr  9169  wdomima2g  9180  fodomfi2  9639  wdomfil  9640  alephiso  9677  iunfictbso  9693  cofsmo  9848  isf32lem10  9941  fin1a2lem7  9985  fodomb  10105  iunfo  10118  tskuni  10362  gruima  10381  gruen  10391  axpre-sup  10748  focdmex  13882  wrdsymb  14062  supcvg  15383  ruclem13  15766  imasval  16970  imasle  16982  imasaddfnlem  16987  imasaddflem  16989  imasvscafn  16996  imasvscaf  16998  imasless  16999  homadm  17500  homacd  17501  dmaf  17509  cdaf  17510  setcepi  17548  imasmnd2  18164  sursubmefmnd  18277  imasgrp2  18432  mhmid  18438  mhmmnd  18439  mhmfmhm  18440  ghmgrp  18441  efgred2  19097  ghmfghm  19170  ghmcyg  19235  gsumval3  19246  gsumzoppg  19283  gsum2dlem2  19310  imasring  19591  znunit  20482  znrrg  20484  cygznlem2a  20486  cygznlem3  20488  cncmp  22243  cnconn  22273  1stcfb  22296  dfac14  22469  qtopval2  22547  qtopuni  22553  qtopid  22556  qtopcld  22564  qtopcn  22565  qtopeu  22567  qtophmeo  22668  elfm3  22801  ovoliunnul  24358  uniiccdif  24429  dchrzrhcl  26080  lgsdchrval  26189  rpvmasumlem  26322  dchrmusum2  26329  dchrvmasumlem3  26334  dchrisum0ff  26342  dchrisum0flblem1  26343  rpvmasum2  26347  dchrisum0re  26348  dchrisum0lem2a  26352  grpocl  28535  grporndm  28545  vafval  28638  smfval  28640  nvgf  28653  vsfval  28668  hhssabloilem  29296  pjhf  29743  elunop  29907  unopf1o  29951  cnvunop  29953  pjinvari  30226  foresf1o  30523  rabfodom  30524  iunrdx  30576  xppreima  30656  gsumpart  30988  qtophaus  31454  sigapildsys  31796  carsgclctunlem3  31953  mtyf  33181  nodense  33581  bdaydm  33655  bdayelon  33657  poimirlem26  35489  poimirlem27  35490  volsupnfl  35508  cocanfo  35562  exidreslem  35721  rngosn3  35768  rngodm1dm2  35776  founiiun  42329  founiiun0  42342  issalnnd  43502  sge0fodjrnlem  43572  ismeannd  43623  caragenunicl  43680  fcores  44176  fcoresf1lem  44177  fcoresf1  44178  fcoresfo  44180  fargshiftfo  44510