Theorem fof 5562

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397   ⊆ wss 3199  ran crn 4728   Fn wfn 5323  ⟶wf 5324  –onto→wfo 5326

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 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212  df-f 5332  df-fo 5334

This theorem is referenced by:  fofun  5563  fofn  5564  dffo2  5566  foima  5567  resdif  5608  ffoss  5619  fconstfvm  5875  cocan2  5934  foeqcnvco  5936  focdmex  6282  algrflem  6399  algrflemg  6400  tposf2  6439  mapsn  6864  ssdomg  6957  fopwdom  7027  fidcenumlemrks  7157  fidcenumlemr  7159  ctmlemr  7312  ctm  7313  ctssdclemn0  7314  ctssdccl  7315  ctssdc  7317  enumctlemm  7318  enumct  7319  fodjuomnilemdc  7348  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  suplocexprlemdisj  7945  suplocexprlemub  7948  wrdsymb  11150  ennnfonelemdc  13043  ennnfonelemg  13047  ennnfonelemp1  13050  ennnfonelemhdmp1  13053  ennnfonelemkh  13056  ennnfonelemhf1o  13057  ennnfonelemex  13058  ennnfonelemhom  13059  ctinfomlemom  13071  ctinf  13074  ctiunctlemudc  13081  ctiunctlemf  13082  omctfn  13087  imasival  13412  imasbas  13413  imasplusg  13414  imasmulr  13415  imasaddfnlemg  13420  imasaddvallemg  13421  imasaddflemg  13422  imasmnd2  13558  imasgrp2  13720  mhmid  13725  mhmmnd  13726  mhmfmhm  13727  ghmgrp  13728  ghmfghm  13936  imasring  14101  znunit  14697  znrrg  14698  dvrecap  15466  gausslemma2dlem1f1o  15818  subctctexmid  16661  pw1nct  16664