Theorem fof 5559

Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
fof	|- ( F : A -onto-> B -> F : A --> B )

Proof of Theorem fof

Step	Hyp	Ref	Expression
1		eqimss 3281	. . 3 |- ( ran F = B -> ran F C_ B )
2	1	anim2i 342	. 2 |- ( ( F Fn A /\ ran F = B ) -> ( F Fn A /\ ran F C_ B ) )
3		df-fo 5332	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4		df-f 5330	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5	2, 3, 4	3imtr4i 201	1 |- ( F : A -onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1397   C_ wss 3200   ran crn 4726   Fn wfn 5321   -->wf 5322   -onto->wfo 5324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-f 5330  df-fo 5332

This theorem is referenced by:  fofun  5560  fofn  5561  dffo2  5563  foima  5564  resdif  5605  ffoss  5616  fconstfvm  5871  cocan2  5928  foeqcnvco  5930  focdmex  6276  algrflem  6393  algrflemg  6394  tposf2  6433  mapsn  6858  ssdomg  6951  fopwdom  7021  fidcenumlemrks  7151  fidcenumlemr  7153  ctmlemr  7306  ctm  7307  ctssdclemn0  7308  ctssdccl  7309  ctssdc  7311  enumctlemm  7312  enumct  7313  fodjuomnilemdc  7342  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  suplocexprlemdisj  7939  suplocexprlemub  7942  wrdsymb  11140  ennnfonelemdc  13019  ennnfonelemg  13023  ennnfonelemp1  13026  ennnfonelemhdmp1  13029  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemhom  13035  ctinfomlemom  13047  ctinf  13050  ctiunctlemudc  13057  ctiunctlemf  13058  omctfn  13063  imasival  13388  imasbas  13389  imasplusg  13390  imasmulr  13391  imasaddfnlemg  13396  imasaddvallemg  13397  imasaddflemg  13398  imasmnd2  13534  imasgrp2  13696  mhmid  13701  mhmmnd  13702  mhmfmhm  13703  ghmgrp  13704  ghmfghm  13912  imasring  14076  znunit  14672  znrrg  14673  dvrecap  15436  gausslemma2dlem1f1o  15788  subctctexmid  16601  pw1nct  16604