Theorem fof 6115

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 3657	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 593	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 5894	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 5892	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 281	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ⊆ wss 3574  ran crn 5115   Fn wfn 5883  ⟶wf 5884  –onto→wfo 5886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-f 5892  df-fo 5894

This theorem is referenced by:  fofun  6116  fofn  6117  dffo2  6119  foima  6120  resdif  6157  fimacnvinrn  6348  fconst5  6471  cocan2  6547  foeqcnvco  6555  soisoi  6578  ffoss  7127  fornex  7135  algrflem  7286  tposf2  7376  smoiso2  7466  mapsn  7899  ssdomg  8001  fopwdom  8068  unfilem2  8225  fodomfib  8240  fofinf1o  8241  brwdomn0  8474  fowdom  8476  wdomtr  8480  wdomima2g  8491  fodomfi2  8883  wdomfil  8884  alephiso  8921  iunfictbso  8937  cofsmo  9091  isf32lem10  9184  fin1a2lem7  9228  fodomb  9348  iunfo  9361  tskuni  9605  gruima  9624  gruen  9634  axpre-sup  9990  focdmex  13139  supcvg  14588  ruclem13  14971  imasval  16171  imasle  16183  imasaddfnlem  16188  imasaddflem  16190  imasvscafn  16197  imasvscaf  16199  imasless  16200  homadm  16690  homacd  16691  dmaf  16699  cdaf  16700  setcepi  16738  imasmnd2  17327  imasgrp2  17530  mhmid  17536  mhmmnd  17537  mhmfmhm  17538  ghmgrp  17539  efgred2  18166  ghmfghm  18236  ghmcyg  18297  gsumval3  18308  gsumzoppg  18344  gsum2dlem2  18370  imasring  18619  znunit  19912  znrrg  19914  cygznlem2a  19916  cygznlem3  19918  cncmp  21195  cnconn  21225  1stcfb  21248  dfac14  21421  qtopval2  21499  qtopuni  21505  qtopid  21508  qtopcld  21516  qtopcn  21517  qtopeu  21519  qtophmeo  21620  elfm3  21754  ovoliunnul  23275  uniiccdif  23346  dchrzrhcl  24970  lgsdchrval  25079  rpvmasumlem  25176  dchrmusum2  25183  dchrvmasumlem3  25188  dchrisum0ff  25196  dchrisum0flblem1  25197  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem2a  25206  grpocl  27354  grporndm  27364  vafval  27458  smfval  27460  nvgf  27473  vsfval  27488  hhssabloilem  28118  pjhf  28567  elunop  28731  unopf1o  28775  cnvunop  28777  pjinvari  29050  foresf1o  29343  rabfodom  29344  iunrdx  29382  xppreima  29449  qtophaus  29903  sigapildsys  30225  carsgclctunlem3  30382  mtyf  31449  nodense  31842  bdaydm  31890  bdayelon  31892  poimirlem26  33435  poimirlem27  33436  volsupnfl  33454  cocanfo  33512  exidreslem  33676  rngosn3  33723  rngodm1dm2  33731  founiiun  39360  founiiun0  39377  mapsnd  39388  issalnnd  40563  sge0fodjrnlem  40633  ismeannd  40684  caragenunicl  40738  fargshiftfo  41378