Theorem fof 5559

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 3281	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 342	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 5332	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 5330	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 201	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397   ⊆ 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  5872  cocan2  5929  foeqcnvco  5931  focdmex  6277  algrflem  6394  algrflemg  6395  tposf2  6434  mapsn  6859  ssdomg  6952  fopwdom  7022  fidcenumlemrks  7152  fidcenumlemr  7154  ctmlemr  7307  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  enumct  7314  fodjuomnilemdc  7343  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  suplocexprlemdisj  7940  suplocexprlemub  7943  wrdsymb  11141  ennnfonelemdc  13021  ennnfonelemg  13025  ennnfonelemp1  13028  ennnfonelemhdmp1  13031  ennnfonelemkh  13034  ennnfonelemhf1o  13035  ennnfonelemex  13036  ennnfonelemhom  13037  ctinfomlemom  13049  ctinf  13052  ctiunctlemudc  13059  ctiunctlemf  13060  omctfn  13065  imasival  13390  imasbas  13391  imasplusg  13392  imasmulr  13393  imasaddfnlemg  13398  imasaddvallemg  13399  imasaddflemg  13400  imasmnd2  13536  imasgrp2  13698  mhmid  13703  mhmmnd  13704  mhmfmhm  13705  ghmgrp  13706  ghmfghm  13914  imasring  14079  znunit  14675  znrrg  14676  dvrecap  15439  gausslemma2dlem1f1o  15791  subctctexmid  16604  pw1nct  16607