Theorem fof 5589

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ⊆ wss 3210  ran crn 4749   Fn wfn 5346  ⟶wf 5347  –onto→wfo 5349

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223  df-f 5355  df-fo 5357

This theorem is referenced by:  fofun  5590  fofn  5591  dffo2  5593  foima  5594  resdif  5635  ffoss  5646  fconstfvm  5901  cocan2  5960  foeqcnvco  5962  focdmex  6307  algrflem  6424  algrflemg  6425  tposf2  6498  mapsn  6924  ssdomg  7017  fopwdom  7088  fidcenumlemrks  7222  fidcenumlemr  7224  ctmlemr  7398  ctm  7399  ctssdclemn0  7400  ctssdccl  7401  ctssdc  7403  enumctlemm  7404  enumct  7405  fodjuomnilemdc  7434  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  suplocexprlemdisj  8031  suplocexprlemub  8034  wrdsymb  11245  ennnfonelemdc  13139  ennnfonelemg  13143  ennnfonelemp1  13146  ennnfonelemhdmp1  13149  ennnfonelemkh  13152  ennnfonelemhf1o  13153  ennnfonelemex  13154  ennnfonelemhom  13155  ctinfomlemom  13167  ctinf  13170  ctiunctlemudc  13177  ctiunctlemf  13178  omctfn  13183  imasival  13508  imasbas  13509  imasplusg  13510  imasmulr  13511  imasaddfnlemg  13516  imasaddvallemg  13517  imasaddflemg  13518  imasmnd2  13654  imasgrp2  13816  mhmid  13821  mhmmnd  13822  mhmfmhm  13823  ghmgrp  13824  ghmfghm  14032  imasring  14197  znunit  14794  znrrg  14795  dvrecap  15565  gausslemma2dlem1f1o  15920  subctctexmid  16761  pw1nct  16764