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

Theorem foima 5628
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 5182 . 2  |-  ( F
" dom  F )  =  ran  F
2 fof 5623 . . . 4  |-  ( F : A -onto-> B  ->  F : A --> B )
3 fdm 5566 . . . 4  |-  ( F : A --> B  ->  dom  F  =  A )
42, 3syl 16 . . 3  |-  ( F : A -onto-> B  ->  dom  F  =  A )
54imaeq2d 5172 . 2  |-  ( F : A -onto-> B  -> 
( F " dom  F )  =  ( F
" A ) )
6 forn 5626 . 2  |-  ( F : A -onto-> B  ->  ran  F  =  B )
71, 5, 63eqtr3a 2499 1  |-  ( F : A -onto-> B  -> 
( F " A
)  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   dom cdm 4843   ran crn 4844   "cima 4846   -->wf 5417   -onto->wfo 5419
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pr 4534
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-br 4296  df-opab 4354  df-xp 4849  df-cnv 4851  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-fn 5424  df-f 5425  df-fo 5427
This theorem is referenced by:  foimacnv  5661  domunfican  7587  fiint  7591  fodomfi  7593  cantnflt2  7884  cantnfp1lem3  7891  cantnflt2OLD  7914  cantnfp1lem3OLD  7917  enfin1ai  8556  symgfixelsi  15943  dprdf1o  16532  lmimlbs  18268  cncmp  18998  cmpfi  19014  cnconn  19029  qtopval2  19272  elfm3  19526  rnelfm  19529  fmfnfmlem2  19531  fmfnfm  19534  eupath2  23604  pjordi  25580  ovoliunnfl  28436  voliunnfl  28438  volsupnfl  28439  ismtybndlem  28708  kelac1  29419  gicabl  29457
  Copyright terms: Public domain W3C validator