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

Theorem fof 6077
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 3641 . . 3 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
21anim2i 592 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
3 df-fo 5858 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4 df-f 5856 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
52, 3, 43imtr4i 281 1 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wss 3559  ran crn 5080   Fn wfn 5847  wf 5848  ontowfo 5850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3566  df-ss 3573  df-f 5856  df-fo 5858
This theorem is referenced by:  fofun  6078  fofn  6079  dffo2  6081  foima  6082  resdif  6119  fimacnvinrn  6309  fconst5  6431  cocan2  6507  foeqcnvco  6515  soisoi  6538  ffoss  7081  fornex  7089  algrflem  7238  tposf2  7328  smoiso2  7418  mapsn  7850  ssdomg  7952  fopwdom  8019  unfilem2  8176  fodomfib  8191  fofinf1o  8192  brwdomn0  8425  fowdom  8427  wdomtr  8431  wdomima2g  8442  fodomfi2  8834  wdomfil  8835  alephiso  8872  iunfictbso  8888  cofsmo  9042  isf32lem10  9135  fin1a2lem7  9179  fodomb  9299  iunfo  9312  tskuni  9556  gruima  9575  gruen  9585  axpre-sup  9941  focdmex  13086  supcvg  14520  ruclem13  14903  imasval  16099  imasle  16111  imasaddfnlem  16116  imasaddflem  16118  imasvscafn  16125  imasvscaf  16127  imasless  16128  homadm  16618  homacd  16619  dmaf  16627  cdaf  16628  setcepi  16666  imasmnd2  17255  imasgrp2  17458  mhmid  17464  mhmmnd  17465  mhmfmhm  17466  ghmgrp  17467  efgred2  18094  ghmfghm  18164  ghmcyg  18225  gsumval3  18236  gsumzoppg  18272  gsum2dlem2  18298  imasring  18547  znunit  19840  znrrg  19842  cygznlem2a  19844  cygznlem3  19846  cncmp  21114  cnconn  21144  1stcfb  21167  dfac14  21340  qtopval2  21418  qtopuni  21424  qtopid  21427  qtopcld  21435  qtopcn  21436  qtopeu  21438  qtophmeo  21539  elfm3  21673  ovoliunnul  23194  uniiccdif  23265  dchrzrhcl  24883  lgsdchrval  24992  rpvmasumlem  25089  dchrmusum2  25096  dchrvmasumlem3  25101  dchrisum0ff  25109  dchrisum0flblem1  25110  rpvmasum2  25114  dchrisum0re  25115  dchrisum0lem2a  25119  grpocl  27221  grporndm  27231  vafval  27325  smfval  27327  nvgf  27340  vsfval  27355  hhssabloilem  27985  pjhf  28434  elunop  28598  unopf1o  28642  cnvunop  28644  pjinvari  28917  foresf1o  29208  rabfodom  29209  iunrdx  29245  xppreima  29309  qtophaus  29703  sigapildsys  30024  carsgclctunlem3  30181  mtyf  31184  bdaydm  31568  poimirlem26  33094  poimirlem27  33095  volsupnfl  33113  cocanfo  33171  exidreslem  33335  rngosn3  33382  rngodm1dm2  33390  founiiun  38857  founiiun0  38874  mapsnd  38885  issalnnd  39891  sge0fodjrnlem  39961  ismeannd  40012  caragenunicl  40066  fargshiftfo  40697
  Copyright terms: Public domain W3C validator