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

Theorem foima 5781
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 5156 . 2  |-  ( F
" dom  F )  =  ran  F
2 fof 5776 . . . 4  |-  ( F : A -onto-> B  ->  F : A --> B )
3 fdm 5716 . . . 4  |-  ( F : A --> B  ->  dom  F  =  A )
42, 3syl 17 . . 3  |-  ( F : A -onto-> B  ->  dom  F  =  A )
54imaeq2d 5146 . 2  |-  ( F : A -onto-> B  -> 
( F " dom  F )  =  ( F
" A ) )
6 forn 5779 . 2  |-  ( F : A -onto-> B  ->  ran  F  =  B )
71, 5, 63eqtr3a 2510 1  |-  ( F : A -onto-> B  -> 
( F " A
)  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1448   dom cdm 4812   ran crn 4813   "cima 4815   -->wf 5557   -onto->wfo 5559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pr 4612
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-br 4375  df-opab 4434  df-xp 4818  df-cnv 4820  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-fn 5564  df-f 5565  df-fo 5567
This theorem is referenced by:  foimacnv  5814  domunfican  7831  fiint  7835  fodomfi  7837  cantnflt2  8165  cantnfp1lem3  8172  enfin1ai  8801  symgfixelsi  17087  dprdf1o  17676  lmimlbs  19405  cncmp  20418  cmpfi  20434  cnconn  20448  qtopval2  20722  elfm3  20976  rnelfm  20979  fmfnfmlem2  20981  fmfnfm  20984  eupath2  25720  pjordi  27838  qtophaus  28670  poimirlem1  31943  poimirlem2  31944  poimirlem3  31945  poimirlem4  31946  poimirlem5  31947  poimirlem6  31948  poimirlem7  31949  poimirlem9  31951  poimirlem10  31952  poimirlem11  31953  poimirlem12  31954  poimirlem14  31956  poimirlem16  31958  poimirlem17  31959  poimirlem19  31961  poimirlem20  31962  poimirlem22  31964  poimirlem23  31965  poimirlem24  31966  poimirlem25  31967  poimirlem29  31971  poimirlem31  31973  ovoliunnfl  31984  voliunnfl  31986  volsupnfl  31987  ismtybndlem  32140  kelac1  35923  gicabl  35959
  Copyright terms: Public domain W3C validator