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

Theorem fof 6028
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 3620 . . 3 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
21anim2i 591 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
3 df-fo 5810 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4 df-f 5808 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
52, 3, 43imtr4i 280 1 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wss 3540  ran crn 5039   Fn wfn 5799  wf 5800  ontowfo 5802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808  df-fo 5810
This theorem is referenced by:  fofun  6029  fofn  6030  dffo2  6032  foima  6033  resdif  6070  fimacnvinrn  6256  fconst5  6376  cocan2  6447  foeqcnvco  6455  soisoi  6478  ffoss  7020  fornex  7028  algrflem  7173  tposf2  7263  smoiso2  7353  mapsn  7785  ssdomg  7887  fopwdom  7953  unfilem2  8110  fodomfib  8125  fofinf1o  8126  brwdomn0  8357  fowdom  8359  wdomtr  8363  wdomima2g  8374  fodomfi2  8766  wdomfil  8767  alephiso  8804  iunfictbso  8820  cofsmo  8974  isf32lem10  9067  fin1a2lem7  9111  fodomb  9229  iunfo  9240  tskuni  9484  gruima  9503  gruen  9513  axpre-sup  9869  focdmex  13001  supcvg  14427  ruclem13  14810  imasval  15994  imasle  16006  imasaddfnlem  16011  imasaddflem  16013  imasvscafn  16020  imasvscaf  16022  imasless  16023  homadm  16513  homacd  16514  dmaf  16522  cdaf  16523  setcepi  16561  imasmnd2  17150  imasgrp2  17353  mhmid  17359  mhmmnd  17360  mhmfmhm  17361  ghmgrp  17362  efgred2  17989  ghmfghm  18059  ghmcyg  18120  gsumval3  18131  gsumzoppg  18167  gsum2dlem2  18193  imasring  18442  znunit  19731  znrrg  19733  cygznlem2a  19735  cygznlem3  19737  cncmp  21005  cnconn  21035  1stcfb  21058  dfac14  21231  qtopval2  21309  qtopuni  21315  qtopid  21318  qtopcld  21326  qtopcn  21327  qtopeu  21329  qtophmeo  21430  elfm3  21564  ovoliunnul  23082  uniiccdif  23152  dchrzrhcl  24770  lgsdchrval  24879  rpvmasumlem  24976  dchrmusum2  24983  dchrvmasumlem3  24988  dchrisum0ff  24996  dchrisum0flblem1  24997  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem2a  25006  fargshiftfo  26166  grpocl  26738  grporndm  26748  vafval  26842  smfval  26844  nvgf  26857  vsfval  26872  hhssabloilem  27502  pjhf  27951  elunop  28115  unopf1o  28159  cnvunop  28161  pjinvari  28434  foresf1o  28727  rabfodom  28728  iunrdx  28764  xppreima  28829  qtophaus  29231  sigapildsys  29552  carsgclctunlem3  29709  mtyf  30703  bdaydm  31077  poimirlem26  32605  poimirlem27  32606  volsupnfl  32624  cocanfo  32682  exidreslem  32846  rngosn3  32893  rngodm1dm2  32901  founiiun  38355  founiiun0  38372  mapsnd  38383  issalnnd  39239  sge0fodjrnlem  39309  ismeannd  39360  caragenunicl  39414
  Copyright terms: Public domain W3C validator