MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fof Structured version   Visualization version   GIF version

Theorem fof 6256
Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
fof (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)

Proof of Theorem fof
StepHypRef Expression
1 eqimss 3806 . . 3 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
21anim2i 603 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
3 df-fo 6037 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4 df-f 6035 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
52, 3, 43imtr4i 281 1 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wss 3723  ran crn 5250   Fn wfn 6026  wf 6027  ontowfo 6029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737  df-f 6035  df-fo 6037
This theorem is referenced by:  fofun  6257  fofn  6258  dffo2  6260  foima  6261  resdif  6298  fimacnvinrn  6491  fconst5  6615  cocan2  6690  foeqcnvco  6698  soisoi  6721  ffoss  7274  fornex  7282  algrflem  7437  tposf2  7528  smoiso2  7619  mapsnd  8051  ssdomg  8155  fopwdom  8224  unfilem2  8381  fodomfib  8396  fofinf1o  8397  brwdomn0  8630  fowdom  8632  wdomtr  8636  wdomima2g  8647  fodomfi2  9083  wdomfil  9084  alephiso  9121  iunfictbso  9137  cofsmo  9293  isf32lem10  9386  fin1a2lem7  9430  fodomb  9550  iunfo  9563  tskuni  9807  gruima  9826  gruen  9836  axpre-sup  10192  focdmex  13343  supcvg  14795  ruclem13  15177  imasval  16379  imasle  16391  imasaddfnlem  16396  imasaddflem  16398  imasvscafn  16405  imasvscaf  16407  imasless  16408  homadm  16897  homacd  16898  dmaf  16906  cdaf  16907  setcepi  16945  imasmnd2  17535  imasgrp2  17738  mhmid  17744  mhmmnd  17745  mhmfmhm  17746  ghmgrp  17747  efgred2  18373  ghmfghm  18443  ghmcyg  18504  gsumval3  18515  gsumzoppg  18551  gsum2dlem2  18577  imasring  18827  znunit  20127  znrrg  20129  cygznlem2a  20131  cygznlem3  20133  cncmp  21416  cnconn  21446  1stcfb  21469  dfac14  21642  qtopval2  21720  qtopuni  21726  qtopid  21729  qtopcld  21737  qtopcn  21738  qtopeu  21740  qtophmeo  21841  elfm3  21974  ovoliunnul  23495  uniiccdif  23566  dchrzrhcl  25191  lgsdchrval  25300  rpvmasumlem  25397  dchrmusum2  25404  dchrvmasumlem3  25409  dchrisum0ff  25417  dchrisum0flblem1  25418  rpvmasum2  25422  dchrisum0re  25423  dchrisum0lem2a  25427  grpocl  27694  grporndm  27704  vafval  27798  smfval  27800  nvgf  27813  vsfval  27828  hhssabloilem  28458  pjhf  28907  elunop  29071  unopf1o  29115  cnvunop  29117  pjinvari  29390  foresf1o  29681  rabfodom  29682  iunrdx  29720  xppreima  29789  qtophaus  30243  sigapildsys  30565  carsgclctunlem3  30722  mtyf  31787  nodense  32179  bdaydm  32227  bdayelon  32229  poimirlem26  33768  poimirlem27  33769  volsupnfl  33787  cocanfo  33844  exidreslem  34008  rngosn3  34055  rngodm1dm2  34063  founiiun  39880  founiiun0  39897  issalnnd  41080  sge0fodjrnlem  41150  ismeannd  41201  caragenunicl  41258  fargshiftfo  41906
  Copyright terms: Public domain W3C validator