Theorem fof 6818

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 3971	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 629	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 6564	. 2 ⊢ (𝐹:𝐴⟶onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 6562	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 295	1 ⊢ (𝐹:𝐴⟶onto𝐵 → 𝐹:𝐴⟶𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3900  ran crn 5656   Fn wfn 6553  ⟶wf 6554  ⟶ontowfo 6556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-f 6562  df-fo 6564

This theorem is used by:  fofun  6819  fofn  6820  dffo2  6822  foima  6823  focnvimacdmdm  6830  focofo  6831  resdif  6868  fimacnvinrn  7095  fompt  7142  fconst5  7235  cocan2  7323  foeqcnvco  7331  soisoi  7359  ffoss  7982  focdmex  7992  opco1  8161  opco2  8162  tposf2  8295  smoiso2  8405  mapfoss  8902  ssdomg  9055  fopwdom  9132  unfilem2  9326  fodomfib  9348  fofinf1o  9349  brwdomn0  9590  fowdom  9592  wdomtr  9596  wdomima2g  9607  fodomfi2  10166  wdomfil  10167  alephiso  10204  iunfictbso  10220  cofsmo  10374  isf32lem10  10467  fin1a2lem7  10511  fodomb  10632  iunfo  10650  tskuni  10895  gruima  10914  gruen  10924  axpre-sup  11281  wrdsymb  14714  supcvg  16054  ruclem13  16439  imasval  17712  imasle  17724  imasaddfnlem  17729  imasaddflem  17731  imasvscafn  17738  imasvscaf  17740  imasless  17741  homadm  18244  homacd  18245  dmaf  18253  cdaf  18254  setcepi  18292  imasmgm2  18892  imasmnd2  18997  sursubmefmnd  19121  imasgrp2  19294  mhmid  19302  mhmmnd  19303  mhmfmhm  19304  ghmgrp  19305  efgred2  19997  ghmfghm  20074  ghmcyg  20140  gsumval3  20151  gsumzoppg  20188  gsum2dlem2  20215  imasring  20590  znunit  21899  znrrg  21901  cygznlem2a  21903  cygznlem3  21905  cncmp  23740  cnconn  23770  1stcfb  23793  dfac14  23967  qtopval2  24045  qtopuni  24051  qtopid  24054  qtopcld  24062  qtopcn  24063  qtopeu  24065  qtophmeo  24166  elfm3  24299  ovoliunnul  25858  uniiccdif  25929  dchrzrhcl  27602  lgsdchrval  27711  rpvmasumlem  27844  dchrmusum2  27851  dchrvmasumlem3  27856  dchrisum0ff  27864  dchrisum0flblem1  27865  rpvmasum2  27869  dchrisum0re  27870  dchrisum0lem2a  27874  nodense  28079  bdaydmOLD  28166  bdayon  28168  om2noseqlt  28715  om2noseqlt2  28716  om2noseqf1o  28717  noseqrdgfn  28722  bdayn0sf1o  28786  grpocl  31132  grporndm  31142  vafval  31235  smfval  31237  nvgf  31250  vsfval  31265  hhssabloilem  31893  pjhf  32340  elunop  32504  unopf1o  32548  cnvunop  32550  pjinvari  32823  foresf1o  33172  rabfodom  33173  iunrdx  33230  xppreima  33311  gsumpart  33694  imasmhm  33985  imasghm  33986  imasrhm  33987  qtophaus  34538  sigapildsys  34865  carsgclctunlem3  35022  werankwe  35821  werankwe2  35822  dfscott3  35827  mtyf  36484  poimirlem26  38756  poimirlem27  38757  volsupnfl  38775  cocanfo  38845  exidreslem  39003  rngosn3  39050  rngodm1dm2  39058  founiiun  46399  founiiun0  46410  issalnnd  47560  sge0fodjrnlem  47631  ismeannd  47682  caragenunicl  47739  fcores  48342  fcoresf1lem  48343  fcoresf1  48344  fcoresfo  48346  3f1oss1  48350  fargshiftfo  48729  uptr2  50542