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

Theorem fof 6569
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 3974 . . 3 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
21anim2i 619 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
3 df-fo 6334 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4 df-f 6332 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
52, 3, 43imtr4i 295 1 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wss 3884  ran crn 5524   Fn wfn 6323  wf 6324  ontowfo 6326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-f 6332  df-fo 6334
This theorem is referenced by:  fofun  6570  fofn  6571  dffo2  6573  foima  6574  resdif  6614  fimacnvinrn  6821  fconst5  6949  cocan2  7030  foeqcnvco  7038  soisoi  7064  ffoss  7633  fornex  7643  algrflem  7806  tposf2  7903  smoiso2  7993  ssdomg  8542  fopwdom  8612  unfilem2  8771  fodomfib  8786  fofinf1o  8787  brwdomn0  9021  fowdom  9023  wdomtr  9027  wdomima2g  9038  fodomfi2  9475  wdomfil  9476  alephiso  9513  iunfictbso  9529  cofsmo  9684  isf32lem10  9777  fin1a2lem7  9821  fodomb  9941  iunfo  9954  tskuni  10198  gruima  10217  gruen  10227  axpre-sup  10584  focdmex  13711  wrdsymb  13889  supcvg  15207  ruclem13  15591  imasval  16780  imasle  16792  imasaddfnlem  16797  imasaddflem  16799  imasvscafn  16806  imasvscaf  16808  imasless  16809  homadm  17296  homacd  17297  dmaf  17305  cdaf  17306  setcepi  17344  imasmnd2  17944  sursubmefmnd  18057  imasgrp2  18210  mhmid  18216  mhmmnd  18217  mhmfmhm  18218  ghmgrp  18219  efgred2  18875  ghmfghm  18948  ghmcyg  19013  gsumval3  19024  gsumzoppg  19061  gsum2dlem2  19088  imasring  19369  znunit  20259  znrrg  20261  cygznlem2a  20263  cygznlem3  20265  cncmp  22001  cnconn  22031  1stcfb  22054  dfac14  22227  qtopval2  22305  qtopuni  22311  qtopid  22314  qtopcld  22322  qtopcn  22323  qtopeu  22325  qtophmeo  22426  elfm3  22559  ovoliunnul  24115  uniiccdif  24186  dchrzrhcl  25833  lgsdchrval  25942  rpvmasumlem  26075  dchrmusum2  26082  dchrvmasumlem3  26087  dchrisum0ff  26095  dchrisum0flblem1  26096  rpvmasum2  26100  dchrisum0re  26101  dchrisum0lem2a  26105  grpocl  28287  grporndm  28297  vafval  28390  smfval  28392  nvgf  28405  vsfval  28420  hhssabloilem  29048  pjhf  29495  elunop  29659  unopf1o  29703  cnvunop  29705  pjinvari  29978  foresf1o  30277  rabfodom  30278  iunrdx  30331  xppreima  30412  gsumpart  30744  qtophaus  31193  sigapildsys  31535  carsgclctunlem3  31692  mtyf  32913  nodense  33310  bdaydm  33358  bdayelon  33360  poimirlem26  35082  poimirlem27  35083  volsupnfl  35101  cocanfo  35155  exidreslem  35314  rngosn3  35361  rngodm1dm2  35369  founiiun  41800  founiiun0  41814  issalnnd  42982  sge0fodjrnlem  43052  ismeannd  43103  caragenunicl  43160  fargshiftfo  43956
  Copyright terms: Public domain W3C validator