Theorem fof 5592

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ⊆ wss 3213  ran crn 4752   Fn wfn 5349  ⟶wf 5350  –onto→wfo 5352

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226  df-f 5358  df-fo 5360

This theorem is referenced by:  fofun  5593  fofn  5594  dffo2  5596  foima  5597  resdif  5638  ffoss  5649  fconstfvm  5904  cocan2  5963  foeqcnvco  5965  focdmex  6310  algrflem  6427  algrflemg  6428  tposf2  6501  mapsn  6927  ssdomg  7020  fopwdom  7091  fidcenumlemrks  7225  fidcenumlemr  7227  ctmlemr  7401  ctm  7402  ctssdclemn0  7403  ctssdccl  7404  ctssdc  7406  enumctlemm  7407  enumct  7408  fodjuomnilemdc  7437  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  suplocexprlemdisj  8040  suplocexprlemub  8043  wrdsymb  11260  ennnfonelemdc  13171  ennnfonelemg  13175  ennnfonelemp1  13178  ennnfonelemhdmp1  13181  ennnfonelemkh  13184  ennnfonelemhf1o  13185  ennnfonelemex  13186  ennnfonelemhom  13187  ctinfomlemom  13199  ctinf  13202  ctiunctlemudc  13209  ctiunctlemf  13210  omctfn  13215  imasival  13540  imasbas  13541  imasplusg  13542  imasmulr  13543  imasaddfnlemg  13548  imasaddvallemg  13549  imasaddflemg  13550  imasmnd2  13686  imasgrp2  13848  mhmid  13853  mhmmnd  13854  mhmfmhm  13855  ghmgrp  13856  ghmfghm  14064  imasring  14229  znunit  14856  znrrg  14857  dvrecap  15627  gausslemma2dlem1f1o  15982  subctctexmid  16823  pw1nct  16826