Theorem fof 5613

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402   ⊆ wss 3220  ran crn 4773   Fn wfn 5370  ⟶wf 5371  –onto→wfo 5373

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-f 5379  df-fo 5381

This theorem is referenced by:  fofun  5614  fofn  5615  dffo2  5617  foima  5618  resdif  5659  ffoss  5670  fconstfvm  5927  cocan2  5988  foeqcnvco  5990  focdmex  6338  algrflem  6459  algrflemg  6460  tposf2  6533  mapfoss  6941  mapsn  6966  ssdomg  7059  fopwdom  7130  fidcenumlemrks  7264  fidcenumlemr  7266  ctmlemr  7442  ctm  7443  ctssdclemn0  7444  ctssdccl  7445  ctssdc  7447  enumctlemm  7448  enumct  7449  fodjuomnilemdc  7478  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  suplocexprlemdisj  8081  suplocexprlemub  8084  wrdsymb  11315  ennnfonelemdc  13273  ennnfonelemg  13277  ennnfonelemp1  13280  ennnfonelemhdmp1  13283  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ennnfonelemex  13288  ennnfonelemhom  13289  ctinfomlemom  13301  ctinf  13304  ctiunctlemudc  13311  ctiunctlemf  13312  omctfn  13317  imasival  13610  imasbas  13611  imasplusg  13612  imasmulr  13613  imasaddfnlemg  13618  imasaddvallemg  13619  imasaddflemg  13620  imasmnd2  13742  imasgrp2  13896  mhmid  13901  mhmmnd  13902  mhmfmhm  13903  ghmgrp  13904  ghmfghm  14113  imasring  14352  znunit  14977  znrrg  14978  dvrecap  15797  gausslemma2dlem1f1o  16162  subctctexmid  17013  pw1nct  17016