MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  foima Structured version   Unicode version

Theorem foima 5815
Description: The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002.)
Assertion
Ref Expression
foima  |-  ( F : A -onto-> B  -> 
( F " A
)  =  B )

Proof of Theorem foima
StepHypRef Expression
1 imadmrn 5197 . 2  |-  ( F
" dom  F )  =  ran  F
2 fof 5810 . . . 4  |-  ( F : A -onto-> B  ->  F : A --> B )
3 fdm 5750 . . . 4  |-  ( F : A --> B  ->  dom  F  =  A )
42, 3syl 17 . . 3  |-  ( F : A -onto-> B  ->  dom  F  =  A )
54imaeq2d 5187 . 2  |-  ( F : A -onto-> B  -> 
( F " dom  F )  =  ( F
" A ) )
6 forn 5813 . 2  |-  ( F : A -onto-> B  ->  ran  F  =  B )
71, 5, 63eqtr3a 2487 1  |-  ( F : A -onto-> B  -> 
( F " A
)  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   dom cdm 4853   ran crn 4854   "cima 4856   -->wf 5597   -onto->wfo 5599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-xp 4859  df-cnv 4861  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-fn 5604  df-f 5605  df-fo 5607
This theorem is referenced by:  foimacnv  5848  domunfican  7853  fiint  7857  fodomfi  7859  cantnflt2  8186  cantnfp1lem3  8193  enfin1ai  8821  symgfixelsi  17075  dprdf1o  17664  lmimlbs  19392  cncmp  20405  cmpfi  20421  cnconn  20435  qtopval2  20709  elfm3  20963  rnelfm  20966  fmfnfmlem2  20968  fmfnfm  20971  eupath2  25706  pjordi  27824  qtophaus  28671  poimirlem1  31905  poimirlem2  31906  poimirlem3  31907  poimirlem4  31908  poimirlem5  31909  poimirlem6  31910  poimirlem7  31911  poimirlem9  31913  poimirlem10  31914  poimirlem11  31915  poimirlem12  31916  poimirlem14  31918  poimirlem16  31920  poimirlem17  31921  poimirlem19  31923  poimirlem20  31924  poimirlem22  31926  poimirlem23  31927  poimirlem24  31928  poimirlem25  31929  poimirlem29  31933  poimirlem31  31935  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  ismtybndlem  32102  kelac1  35891  gicabl  35927
  Copyright terms: Public domain W3C validator