Theorem fof 6788

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3899  ran crn 5652   Fn wfn 6526  ⟶wf 6527  –onto→wfo 6529

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916  df-f 6535  df-fo 6537

This theorem is used by:  fofun  6789  fofn  6790  dffo2  6792  foima  6793  focnvimacdmdm  6800  focofo  6801  resdif  6838  fimacnvinrn  7063  fompt  7110  fconst5  7204  cocan2  7292  foeqcnvco  7300  soisoi  7328  ffoss  7947  focdmex  7957  opco1  8123  opco2  8124  tposf2  8251  smoiso2  8361  mapfoss  8858  ssdomg  9011  fopwdom  9088  unfilem2  9282  fodomfib  9304  fofinf1o  9305  brwdomn0  9547  fowdom  9549  wdomtr  9553  wdomima2g  9564  fodomfi2  10120  wdomfil  10121  alephiso  10158  iunfictbso  10174  cofsmo  10328  isf32lem10  10421  fin1a2lem7  10465  fodomb  10586  iunfo  10604  tskuni  10849  gruima  10868  gruen  10878  axpre-sup  11235  wrdsymb  14667  supcvg  16005  ruclem13  16390  imasval  17663  imasle  17675  imasaddfnlem  17680  imasaddflem  17682  imasvscafn  17689  imasvscaf  17691  imasless  17692  homadm  18195  homacd  18196  dmaf  18204  cdaf  18205  setcepi  18243  imasmgm2  18843  imasmnd2  18948  sursubmefmnd  19072  imasgrp2  19245  mhmid  19253  mhmmnd  19254  mhmfmhm  19255  ghmgrp  19256  efgred2  19947  ghmfghm  20024  ghmcyg  20090  gsumval3  20101  gsumzoppg  20138  gsum2dlem2  20165  imasring  20540  znunit  21849  znrrg  21851  cygznlem2a  21853  cygznlem3  21855  cncmp  23690  cnconn  23720  1stcfb  23743  dfac14  23917  qtopval2  23995  qtopuni  24001  qtopid  24004  qtopcld  24012  qtopcn  24013  qtopeu  24015  qtophmeo  24116  elfm3  24249  ovoliunnul  25808  uniiccdif  25879  dchrzrhcl  27554  lgsdchrval  27663  rpvmasumlem  27796  dchrmusum2  27803  dchrvmasumlem3  27808  dchrisum0ff  27816  dchrisum0flblem1  27817  rpvmasum2  27821  dchrisum0re  27822  dchrisum0lem2a  27826  nodense  28031  bdaydmOLD  28118  bdayon  28120  om2noseqlt  28667  om2noseqlt2  28668  om2noseqf1o  28669  noseqrdgfn  28674  bdayn0sf1o  28738  grpocl  31084  grporndm  31094  vafval  31187  smfval  31189  nvgf  31202  vsfval  31217  hhssabloilem  31845  pjhf  32292  elunop  32456  unopf1o  32500  cnvunop  32502  pjinvari  32775  foresf1o  33082  rabfodom  33083  iunrdx  33140  xppreima  33221  gsumpart  33606  imasmhm  33897  imasghm  33898  imasrhm  33899  qtophaus  34450  sigapildsys  34777  carsgclctunlem3  34935  dfscott3  35721  mtyf  36286  poimirlem26  38532  poimirlem27  38533  volsupnfl  38551  cocanfo  38621  exidreslem  38779  rngosn3  38826  rngodm1dm2  38834  founiiun  46137  founiiun0  46148  issalnnd  47299  sge0fodjrnlem  47370  ismeannd  47421  caragenunicl  47478  fcores  48081  fcoresf1lem  48082  fcoresf1  48083  fcoresfo  48085  3f1oss1  48089  fargshiftfo  48468  uptr2  50273