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

Theorem fof 6757
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 4001 . . 3 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
21anim2i 618 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
3 df-fo 6503 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4 df-f 6501 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
52, 3, 43imtr4i 292 1 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wss 3911  ran crn 5635   Fn wfn 6492  wf 6493  ontowfo 6495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-f 6501  df-fo 6503
This theorem is referenced by:  fofun  6758  fofn  6759  dffo2  6761  foima  6762  focnvimacdmdm  6769  focofo  6770  resdif  6806  fimacnvinrn  7023  fconst5  7156  cocan2  7239  foeqcnvco  7247  soisoi  7274  ffoss  7879  focdmex  7889  opco1  8056  opco2  8057  tposf2  8182  smoiso2  8316  mapfoss  8791  ssdomg  8941  fopwdom  9025  unfilem2  9256  fodomfib  9271  fofinf1o  9272  brwdomn0  9506  fowdom  9508  wdomtr  9512  wdomima2g  9523  fodomfi2  9997  wdomfil  9998  alephiso  10035  iunfictbso  10051  cofsmo  10206  isf32lem10  10299  fin1a2lem7  10343  fodomb  10463  iunfo  10476  tskuni  10720  gruima  10739  gruen  10749  axpre-sup  11106  wrdsymb  14431  supcvg  15742  ruclem13  16125  imasval  17394  imasle  17406  imasaddfnlem  17411  imasaddflem  17413  imasvscafn  17420  imasvscaf  17422  imasless  17423  homadm  17927  homacd  17928  dmaf  17936  cdaf  17937  setcepi  17975  imasmnd2  18594  sursubmefmnd  18707  imasgrp2  18863  mhmid  18869  mhmmnd  18870  mhmfmhm  18871  ghmgrp  18872  efgred2  19536  ghmfghm  19610  ghmcyg  19674  gsumval3  19685  gsumzoppg  19722  gsum2dlem2  19749  imasring  20046  znunit  20973  znrrg  20975  cygznlem2a  20977  cygznlem3  20979  cncmp  22746  cnconn  22776  1stcfb  22799  dfac14  22972  qtopval2  23050  qtopuni  23056  qtopid  23059  qtopcld  23067  qtopcn  23068  qtopeu  23070  qtophmeo  23171  elfm3  23304  ovoliunnul  24874  uniiccdif  24945  dchrzrhcl  26596  lgsdchrval  26705  rpvmasumlem  26838  dchrmusum2  26845  dchrvmasumlem3  26850  dchrisum0ff  26858  dchrisum0flblem1  26859  rpvmasum2  26863  dchrisum0re  26864  dchrisum0lem2a  26868  nodense  27043  bdaydm  27117  bdayelon  27119  grpocl  29445  grporndm  29455  vafval  29548  smfval  29550  nvgf  29563  vsfval  29578  hhssabloilem  30206  pjhf  30653  elunop  30817  unopf1o  30861  cnvunop  30863  pjinvari  31136  foresf1o  31434  rabfodom  31435  iunrdx  31485  xppreima  31565  gsumpart  31900  qtophaus  32420  sigapildsys  32764  carsgclctunlem3  32923  mtyf  34149  poimirlem26  36107  poimirlem27  36108  volsupnfl  36126  cocanfo  36180  exidreslem  36339  rngosn3  36386  rngodm1dm2  36394  founiiun  43403  founiiun0  43416  issalnnd  44593  sge0fodjrnlem  44664  ismeannd  44715  caragenunicl  44772  fcores  45308  fcoresf1lem  45309  fcoresf1  45310  fcoresfo  45312  fargshiftfo  45641
  Copyright terms: Public domain W3C validator