Theorem fof 6590

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 4023	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 618	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6361	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6359	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 294	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ⊆ wss 3936  ran crn 5556   Fn wfn 6350  ⟶wf 6351  –onto→wfo 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-f 6359  df-fo 6361

This theorem is referenced by:  fofun  6591  fofn  6592  dffo2  6594  foima  6595  resdif  6635  fimacnvinrn  6840  fconst5  6968  cocan2  7048  foeqcnvco  7056  soisoi  7081  ffoss  7647  fornex  7657  algrflem  7819  tposf2  7916  smoiso2  8006  ssdomg  8555  fopwdom  8625  unfilem2  8783  fodomfib  8798  fofinf1o  8799  brwdomn0  9033  fowdom  9035  wdomtr  9039  wdomima2g  9050  fodomfi2  9486  wdomfil  9487  alephiso  9524  iunfictbso  9540  cofsmo  9691  isf32lem10  9784  fin1a2lem7  9828  fodomb  9948  iunfo  9961  tskuni  10205  gruima  10224  gruen  10234  axpre-sup  10591  focdmex  13712  wrdsymb  13893  supcvg  15211  ruclem13  15595  imasval  16784  imasle  16796  imasaddfnlem  16801  imasaddflem  16803  imasvscafn  16810  imasvscaf  16812  imasless  16813  homadm  17300  homacd  17301  dmaf  17309  cdaf  17310  setcepi  17348  imasmnd2  17948  sursubmefmnd  18061  imasgrp2  18214  mhmid  18220  mhmmnd  18221  mhmfmhm  18222  ghmgrp  18223  efgred2  18879  ghmfghm  18951  ghmcyg  19016  gsumval3  19027  gsumzoppg  19064  gsum2dlem2  19091  imasring  19369  znunit  20710  znrrg  20712  cygznlem2a  20714  cygznlem3  20716  cncmp  22000  cnconn  22030  1stcfb  22053  dfac14  22226  qtopval2  22304  qtopuni  22310  qtopid  22313  qtopcld  22321  qtopcn  22322  qtopeu  22324  qtophmeo  22425  elfm3  22558  ovoliunnul  24108  uniiccdif  24179  dchrzrhcl  25821  lgsdchrval  25930  rpvmasumlem  26063  dchrmusum2  26070  dchrvmasumlem3  26075  dchrisum0ff  26083  dchrisum0flblem1  26084  rpvmasum2  26088  dchrisum0re  26089  dchrisum0lem2a  26093  grpocl  28277  grporndm  28287  vafval  28380  smfval  28382  nvgf  28395  vsfval  28410  hhssabloilem  29038  pjhf  29485  elunop  29649  unopf1o  29693  cnvunop  29695  pjinvari  29968  foresf1o  30265  rabfodom  30266  iunrdx  30315  xppreima  30394  qtophaus  31100  sigapildsys  31421  carsgclctunlem3  31578  mtyf  32799  nodense  33196  bdaydm  33244  bdayelon  33246  poimirlem26  34933  poimirlem27  34934  volsupnfl  34952  cocanfo  35008  exidreslem  35170  rngosn3  35217  rngodm1dm2  35225  founiiun  41484  founiiun0  41500  issalnnd  42677  sge0fodjrnlem  42747  ismeannd  42798  caragenunicl  42855  fargshiftfo  43651