Theorem fof 5345

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 3151	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 339	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 5129	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 5127	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 200	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331   ⊆ wss 3071  ran crn 4540   Fn wfn 5118  ⟶wf 5119  –onto→wfo 5121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084  df-f 5127  df-fo 5129

This theorem is referenced by:  fofun  5346  fofn  5347  dffo2  5349  foima  5350  resdif  5389  ffoss  5399  fconstfvm  5638  cocan2  5689  foeqcnvco  5691  fornex  6013  algrflem  6126  algrflemg  6127  tposf2  6165  mapsn  6584  ssdomg  6672  fopwdom  6730  fidcenumlemrks  6841  fidcenumlemr  6843  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumctlemm  6999  enumct  7000  fodjuomnilemdc  7016  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  suplocexprlemdisj  7528  suplocexprlemub  7531  focdmex  10533  ennnfonelemdc  11912  ennnfonelemg  11916  ennnfonelemp1  11919  ennnfonelemhdmp1  11922  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemex  11927  ennnfonelemhom  11928  ctinfomlemom  11940  ctinf  11943  ctiunctlemudc  11950  ctiunctlemf  11951  dvrecap  12846  subctctexmid  13196