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

Theorem elpreima 5826
Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
elpreima  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  <->  ( B  e.  A  /\  ( F `  B )  e.  C ) ) )

Proof of Theorem elpreima
StepHypRef Expression
1 cnvimass 5192 . . . . 5  |-  ( `' F " C ) 
C_  dom  F
21sseli 3355 . . . 4  |-  ( B  e.  ( `' F " C )  ->  B  e.  dom  F )
3 fndm 5513 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2510 . . . 4  |-  ( F  Fn  A  ->  ( B  e.  dom  F  <->  B  e.  A ) )
52, 4syl5ib 219 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  ->  B  e.  A )
)
6 fnfun 5511 . . . . 5  |-  ( F  Fn  A  ->  Fun  F )
7 fvimacnvi 5820 . . . . 5  |-  ( ( Fun  F  /\  B  e.  ( `' F " C ) )  -> 
( F `  B
)  e.  C )
86, 7sylan 471 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  ( `' F " C ) )  ->  ( F `  B )  e.  C
)
98ex 434 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( F `  B
)  e.  C ) )
105, 9jcad 533 . 2  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( B  e.  A  /\  ( F `  B
)  e.  C ) ) )
11 fvimacnv 5821 . . . . 5  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1211funfni 5514 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1312biimpd 207 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  ->  B  e.  ( `' F " C ) ) )
1413expimpd 603 . 2  |-  ( F  Fn  A  ->  (
( B  e.  A  /\  ( F `  B
)  e.  C )  ->  B  e.  ( `' F " C ) ) )
1510, 14impbid 191 1  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  <->  ( B  e.  A  /\  ( F `  B )  e.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1756   `'ccnv 4842   dom cdm 4843   "cima 4846   Fun wfun 5415    Fn wfn 5416   ` cfv 5421
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-sbc 3190  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-uni 4095  df-br 4296  df-opab 4354  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-fv 5429
This theorem is referenced by:  fniniseg  5827  fncnvima2  5828  rexsuppOLD  5831  unpreima  5832  respreima  5835  suppssOLD  5839  suppssrOLD  5840  fnse  6692  brwitnlem  6950  wemapso2OLD  7769  unxpwdom2  7806  cantnfleOLD  7912  cantnfp1lem2OLD  7916  cantnfp1lem3OLD  7917  cantnfp1OLD  7918  cantnflem1aOLD  7919  cantnflem1cOLD  7921  cantnflem3OLD  7924  mapfienOLD  7930  cnfcomlemOLD  7943  cnfcom3OLD  7948  smobeth  8753  fpwwe2lem6  8805  fpwwe2lem9  8808  hashkf  12108  isercolllem2  13146  isercolllem3  13147  isercoll  13148  fsumss  13205  tanval  13415  1arith  13991  0ram  14084  ghmpreima  15771  ghmnsgpreima  15774  torsubg  16339  kerf1hrm  16834  lmhmpreima  17132  evlslem3  17603  mpfind  17625  znunithash  18000  cncnpi  18885  cncnp  18887  cnpdis  18900  cnt0  18953  cnhaus  18961  2ndcomap  19065  1stccnp  19069  ptpjpre1  19147  tx1cn  19185  tx2cn  19186  txcnmpt  19200  txdis1cn  19211  hauseqlcld  19222  xkoptsub  19230  xkococn  19236  kqsat  19307  kqcldsat  19309  kqreglem1  19317  kqreglem2  19318  reghmph  19369  ordthmeolem  19377  tmdcn2  19663  clssubg  19682  tgphaus  19690  divstgplem  19694  ucncn  19863  xmeterval  20010  imasf1obl  20066  blval2  20153  metuel2  20157  isnghm  20305  cnbl0  20356  cnblcld  20357  cnheiborlem  20529  nmhmcn  20678  ismbl  21012  mbfeqalem  21123  mbfmulc2lem  21128  mbfmax  21130  mbfposr  21133  mbfimaopnlem  21136  mbfaddlem  21141  mbfsup  21145  i1f1lem  21170  i1fpos  21187  mbfi1fseqlem4  21199  itg2monolem1  21231  itg2gt0  21241  itg2cnlem1  21242  itg2cnlem2  21243  plyeq0lem  21681  dgrlem  21700  dgrub  21705  dgrlb  21707  pserulm  21890  psercnlem2  21892  psercnlem1  21893  psercn  21894  abelth  21909  eff1olem  22007  ellogrn  22014  dvloglem  22096  logf1o2  22098  efopnlem1  22104  efopnlem2  22105  logtayl  22108  cxpcn3lem  22188  cxpcn3  22189  resqrcn  22190  asinneg  22284  areambl  22355  sqff1o  22523  ubthlem1  24274  unipreima  25964  1stpreima  26004  2ndpreima  26005  suppss3  26030  kerunit  26294  cnre2csqlem  26343  elzrhunit  26411  qqhval2lem  26413  qqhf  26418  1stmbfm  26678  2ndmbfm  26679  mbfmcnt  26686  eulerpartlemsv2  26744  eulerpartlemv  26750  eulerpartlemf  26756  eulerpartlemgvv  26762  eulerpartlemgh  26764  eulerpartlemgs2  26766  sseqmw  26777  sseqf  26778  sseqp1  26781  fiblem  26784  fibp1  26787  cvmseu  27168  cvmliftmolem1  27173  cvmliftmolem2  27174  cvmliftlem15  27190  cvmlift2lem10  27204  cvmlift3lem8  27218  fprodss  27464  cnambfre  28443  dvtan  28445  ftc1anclem3  28472  ftc1anclem5  28474  areacirc  28492  sstotbnd2  28676  keridl  28835  pw2f1ocnv  29389  rfcnpre1  29744  rfcnpre2  29756  rfcnpre3  29758  rfcnpre4  29759  ellkr  32737
  Copyright terms: Public domain W3C validator