Theorem fof 5556

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ⊆ wss 3198  ran crn 4724   Fn wfn 5319  ⟶wf 5320  –onto→wfo 5322

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211  df-f 5328  df-fo 5330

This theorem is referenced by:  fofun  5557  fofn  5558  dffo2  5560  foima  5561  resdif  5602  ffoss  5612  fconstfvm  5867  cocan2  5924  foeqcnvco  5926  focdmex  6272  algrflem  6389  algrflemg  6390  tposf2  6429  mapsn  6854  ssdomg  6947  fopwdom  7017  fidcenumlemrks  7146  fidcenumlemr  7148  ctmlemr  7301  ctm  7302  ctssdclemn0  7303  ctssdccl  7304  ctssdc  7306  enumctlemm  7307  enumct  7308  fodjuomnilemdc  7337  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  suplocexprlemdisj  7933  suplocexprlemub  7936  wrdsymb  11134  ennnfonelemdc  13013  ennnfonelemg  13017  ennnfonelemp1  13020  ennnfonelemhdmp1  13023  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ennnfonelemex  13028  ennnfonelemhom  13029  ctinfomlemom  13041  ctinf  13044  ctiunctlemudc  13051  ctiunctlemf  13052  omctfn  13057  imasival  13382  imasbas  13383  imasplusg  13384  imasmulr  13385  imasaddfnlemg  13390  imasaddvallemg  13391  imasaddflemg  13392  imasmnd2  13528  imasgrp2  13690  mhmid  13695  mhmmnd  13696  mhmfmhm  13697  ghmgrp  13698  ghmfghm  13906  imasring  14070  znunit  14666  znrrg  14667  dvrecap  15430  gausslemma2dlem1f1o  15782  subctctexmid  16551  pw1nct  16554