Theorem fof 6153

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 3690	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 592	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 5932	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 5930	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 281	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ⊆ wss 3607  ran crn 5144   Fn wfn 5921  ⟶wf 5922  –onto→wfo 5924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930  df-fo 5932

This theorem is referenced by:  fofun  6154  fofn  6155  dffo2  6157  foima  6158  resdif  6195  fimacnvinrn  6388  fconst5  6512  cocan2  6587  foeqcnvco  6595  soisoi  6618  ffoss  7169  fornex  7177  algrflem  7331  tposf2  7421  smoiso2  7511  mapsn  7941  ssdomg  8043  fopwdom  8109  unfilem2  8266  fodomfib  8281  fofinf1o  8282  brwdomn0  8515  fowdom  8517  wdomtr  8521  wdomima2g  8532  fodomfi2  8921  wdomfil  8922  alephiso  8959  iunfictbso  8975  cofsmo  9129  isf32lem10  9222  fin1a2lem7  9266  fodomb  9386  iunfo  9399  tskuni  9643  gruima  9662  gruen  9672  axpre-sup  10028  focdmex  13179  supcvg  14632  ruclem13  15015  imasval  16218  imasle  16230  imasaddfnlem  16235  imasaddflem  16237  imasvscafn  16244  imasvscaf  16246  imasless  16247  homadm  16737  homacd  16738  dmaf  16746  cdaf  16747  setcepi  16785  imasmnd2  17374  imasgrp2  17577  mhmid  17583  mhmmnd  17584  mhmfmhm  17585  ghmgrp  17586  efgred2  18212  ghmfghm  18282  ghmcyg  18343  gsumval3  18354  gsumzoppg  18390  gsum2dlem2  18416  imasring  18665  znunit  19960  znrrg  19962  cygznlem2a  19964  cygznlem3  19966  cncmp  21243  cnconn  21273  1stcfb  21296  dfac14  21469  qtopval2  21547  qtopuni  21553  qtopid  21556  qtopcld  21564  qtopcn  21565  qtopeu  21567  qtophmeo  21668  elfm3  21801  ovoliunnul  23321  uniiccdif  23392  dchrzrhcl  25015  lgsdchrval  25124  rpvmasumlem  25221  dchrmusum2  25228  dchrvmasumlem3  25233  dchrisum0ff  25241  dchrisum0flblem1  25242  rpvmasum2  25246  dchrisum0re  25247  dchrisum0lem2a  25251  grpocl  27482  grporndm  27492  vafval  27586  smfval  27588  nvgf  27601  vsfval  27616  hhssabloilem  28246  pjhf  28695  elunop  28859  unopf1o  28903  cnvunop  28905  pjinvari  29178  foresf1o  29469  rabfodom  29470  iunrdx  29508  xppreima  29577  qtophaus  30031  sigapildsys  30353  carsgclctunlem3  30510  mtyf  31575  nodense  31967  bdaydm  32015  bdayelon  32017  poimirlem26  33565  poimirlem27  33566  volsupnfl  33584  cocanfo  33642  exidreslem  33806  rngosn3  33853  rngodm1dm2  33861  founiiun  39674  founiiun0  39691  mapsnd  39702  issalnnd  40881  sge0fodjrnlem  40951  ismeannd  41002  caragenunicl  41059  fargshiftfo  41703