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  11142  ennnfonelemdc  13022  ennnfonelemg  13026  ennnfonelemp1  13029  ennnfonelemhdmp1  13032  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ennnfonelemex  13037  ennnfonelemhom  13038  ctinfomlemom  13050  ctinf  13053  ctiunctlemudc  13060  ctiunctlemf  13061  omctfn  13066  imasival  13391  imasbas  13392  imasplusg  13393  imasmulr  13394  imasaddfnlemg  13399  imasaddvallemg  13400  imasaddflemg  13401  imasmnd2  13537  imasgrp2  13699  mhmid  13704  mhmmnd  13705  mhmfmhm  13706  ghmgrp  13707  ghmfghm  13915  imasring  14080  znunit  14676  znrrg  14677  dvrecap  15440  gausslemma2dlem1f1o  15792  subctctexmid  16622  pw1nct  16625