Theorem fof 5450

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1363   ⊆ wss 3141  ran crn 4639   Fn wfn 5223  ⟶wf 5224  –onto→wfo 5226

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154  df-f 5232  df-fo 5234

This theorem is referenced by:  fofun  5451  fofn  5452  dffo2  5454  foima  5455  resdif  5495  ffoss  5505  fconstfvm  5747  cocan2  5802  foeqcnvco  5804  focdmex  6130  algrflem  6244  algrflemg  6245  tposf2  6283  mapsn  6704  ssdomg  6792  fopwdom  6850  fidcenumlemrks  6966  fidcenumlemr  6968  ctmlemr  7121  ctm  7122  ctssdclemn0  7123  ctssdccl  7124  ctssdc  7126  enumctlemm  7127  enumct  7128  fodjuomnilemdc  7156  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  suplocexprlemdisj  7733  suplocexprlemub  7736  ennnfonelemdc  12414  ennnfonelemg  12418  ennnfonelemp1  12421  ennnfonelemhdmp1  12424  ennnfonelemkh  12427  ennnfonelemhf1o  12428  ennnfonelemex  12429  ennnfonelemhom  12430  ctinfomlemom  12442  ctinf  12445  ctiunctlemudc  12452  ctiunctlemf  12453  omctfn  12458  imasival  12745  imasbas  12746  imasplusg  12747  imasmulr  12748  imasaddfnlemg  12753  imasaddvallemg  12754  imasaddflemg  12755  imasgrp2  13013  mhmid  13018  mhmmnd  13019  mhmfmhm  13020  ghmgrp  13021  imasring  13369  dvrecap  14530  subctctexmid  15104  pw1nct  15106