Theorem fof 6772

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3914  ran crn 5639   Fn wfn 6506  ⟶wf 6507  –onto→wfo 6509

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 3931  df-f 6515  df-fo 6517

This theorem is referenced by:  fofun  6773  fofn  6774  dffo2  6776  foima  6777  focnvimacdmdm  6784  focofo  6785  resdif  6821  fimacnvinrn  7043  fompt  7090  fconst5  7180  cocan2  7267  foeqcnvco  7275  soisoi  7303  ffoss  7924  focdmex  7934  opco1  8102  opco2  8103  tposf2  8229  smoiso2  8338  mapfoss  8825  ssdomg  8971  fopwdom  9049  unfilem2  9255  fodomfib  9280  fodomfibOLD  9282  fofinf1o  9283  brwdomn0  9522  fowdom  9524  wdomtr  9528  wdomima2g  9539  fodomfi2  10013  wdomfil  10014  alephiso  10051  iunfictbso  10067  cofsmo  10222  isf32lem10  10315  fin1a2lem7  10359  fodomb  10479  iunfo  10492  tskuni  10736  gruima  10755  gruen  10765  axpre-sup  11122  wrdsymb  14507  supcvg  15822  ruclem13  16210  imasval  17474  imasle  17486  imasaddfnlem  17491  imasaddflem  17493  imasvscafn  17500  imasvscaf  17502  imasless  17503  homadm  18002  homacd  18003  dmaf  18011  cdaf  18012  setcepi  18050  imasmnd2  18701  sursubmefmnd  18823  imasgrp2  18987  mhmid  18995  mhmmnd  18996  mhmfmhm  18997  ghmgrp  18998  efgred2  19683  ghmfghm  19760  ghmcyg  19826  gsumval3  19837  gsumzoppg  19874  gsum2dlem2  19901  imasring  20239  znunit  21473  znrrg  21475  cygznlem2a  21477  cygznlem3  21479  cncmp  23279  cnconn  23309  1stcfb  23332  dfac14  23505  qtopval2  23583  qtopuni  23589  qtopid  23592  qtopcld  23600  qtopcn  23601  qtopeu  23603  qtophmeo  23704  elfm3  23837  ovoliunnul  25408  uniiccdif  25479  dchrzrhcl  27156  lgsdchrval  27265  rpvmasumlem  27398  dchrmusum2  27405  dchrvmasumlem3  27410  dchrisum0ff  27418  dchrisum0flblem1  27419  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem2a  27428  nodense  27604  bdaydm  27686  bdayelon  27688  om2noseqlt  28193  om2noseqlt2  28194  om2noseqf1o  28195  noseqrdgfn  28200  bdayn0sf1o  28259  grpocl  30429  grporndm  30439  vafval  30532  smfval  30534  nvgf  30547  vsfval  30562  hhssabloilem  31190  pjhf  31637  elunop  31801  unopf1o  31845  cnvunop  31847  pjinvari  32120  foresf1o  32433  rabfodom  32434  iunrdx  32492  xppreima  32569  gsumpart  32997  imasmhm  33325  imasghm  33326  imasrhm  33327  qtophaus  33826  sigapildsys  34152  carsgclctunlem3  34311  mtyf  35539  poimirlem26  37640  poimirlem27  37641  volsupnfl  37659  cocanfo  37713  exidreslem  37871  rngosn3  37918  rngodm1dm2  37926  founiiun  45173  founiiun0  45184  issalnnd  46343  sge0fodjrnlem  46414  ismeannd  46465  caragenunicl  46522  fcores  47068  fcoresf1lem  47069  fcoresf1  47070  fcoresfo  47072  3f1oss1  47076  fargshiftfo  47443  uptr2  49210