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

Theorem elpreima 5909
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 5269 . . . . 5  |-  ( `' F " C ) 
C_  dom  F
21sseli 3413 . . . 4  |-  ( B  e.  ( `' F " C )  ->  B  e.  dom  F )
3 fndm 5588 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2452 . . . 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 5586 . . . . 5  |-  ( F  Fn  A  ->  Fun  F )
7 fvimacnvi 5903 . . . . 5  |-  ( ( Fun  F  /\  B  e.  ( `' F " C ) )  -> 
( F `  B
)  e.  C )
86, 7sylan 469 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  ( `' F " C ) )  ->  ( F `  B )  e.  C
)
98ex 432 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( F `  B
)  e.  C ) )
105, 9jcad 531 . 2  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( B  e.  A  /\  ( F `  B
)  e.  C ) ) )
11 fvimacnv 5904 . . . . 5  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1211funfni 5589 . . . 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 601 . 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 367    e. wcel 1826   `'ccnv 4912   dom cdm 4913   "cima 4916   Fun wfun 5490    Fn wfn 5491   ` cfv 5496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-fv 5504
This theorem is referenced by:  fniniseg  5910  fncnvima2  5911  rexsuppOLD  5914  unpreima  5915  respreima  5918  suppssOLD  5922  suppssrOLD  5923  fnse  6816  brwitnlem  7075  wemapso2OLD  7892  unxpwdom2  7929  cantnfleOLD  8033  cantnfp1lem2OLD  8037  cantnfp1lem3OLD  8038  cantnfp1OLD  8039  cantnflem1aOLD  8040  cantnflem1cOLD  8042  cantnflem3OLD  8045  mapfienOLD  8051  cnfcomlemOLD  8064  cnfcom3OLD  8069  smobeth  8874  fpwwe2lem6  8924  fpwwe2lem9  8927  hashkf  12309  isercolllem2  13490  isercolllem3  13491  isercoll  13492  fsumss  13549  fprodss  13757  tanval  13865  1arith  14447  0ram  14540  ghmpreima  16405  ghmnsgpreima  16408  torsubg  16977  kerf1hrm  17505  lmhmpreima  17807  evlslem3  18296  mpfind  18318  znunithash  18694  cncnpi  19865  cncnp  19867  cnpdis  19880  cnt0  19933  cnhaus  19941  2ndcomap  20044  1stccnp  20048  ptpjpre1  20157  tx1cn  20195  tx2cn  20196  txcnmpt  20210  txdis1cn  20221  hauseqlcld  20232  xkoptsub  20240  xkococn  20246  kqsat  20317  kqcldsat  20319  kqreglem1  20327  kqreglem2  20328  reghmph  20379  ordthmeolem  20387  tmdcn2  20673  clssubg  20692  tgphaus  20700  qustgplem  20704  ucncn  20873  xmeterval  21020  imasf1obl  21076  blval2  21163  metuel2  21167  isnghm  21315  cnbl0  21366  cnblcld  21367  cnheiborlem  21539  nmhmcn  21688  ismbl  22022  mbfeqalem  22134  mbfmulc2lem  22139  mbfmax  22141  mbfposr  22144  mbfimaopnlem  22147  mbfaddlem  22152  mbfsup  22156  i1f1lem  22181  i1fpos  22198  mbfi1fseqlem4  22210  itg2monolem1  22242  itg2gt0  22252  itg2cnlem1  22253  itg2cnlem2  22254  plyeq0lem  22692  dgrlem  22711  dgrub  22716  dgrlb  22718  pserulm  22902  psercnlem2  22904  psercnlem1  22905  psercn  22906  abelth  22921  eff1olem  23020  ellogrn  23032  dvloglem  23116  logf1o2  23118  efopnlem1  23124  efopnlem2  23125  logtayl  23128  cxpcn3lem  23208  cxpcn3  23209  resqrtcn  23210  asinneg  23333  areambl  23405  sqff1o  23573  ubthlem1  25903  unipreima  27624  1stpreima  27672  2ndpreima  27673  suppss3  27700  kerunit  27967  cnre2csqlem  28046  elzrhunit  28113  qqhval2lem  28115  qqhf  28120  1stmbfm  28387  2ndmbfm  28388  mbfmcnt  28395  eulerpartlemsv2  28480  eulerpartlemv  28486  eulerpartlemf  28492  eulerpartlemgvv  28498  eulerpartlemgh  28500  eulerpartlemgs2  28502  sseqmw  28513  sseqf  28514  sseqp1  28517  fiblem  28520  fibp1  28523  cvmseu  28910  cvmliftmolem1  28915  cvmliftmolem2  28916  cvmliftlem15  28932  cvmlift2lem10  28946  cvmlift3lem8  28960  elmthm  29125  mthmblem  29129  mclsppslem  29132  mclspps  29133  cnambfre  30228  dvtan  30231  ftc1anclem3  30258  ftc1anclem5  30260  areacirc  30278  sstotbnd2  30436  keridl  30595  pw2f1ocnv  31145  binomcxplemdvbinom  31426  binomcxplemcvg  31427  binomcxplemnotnn0  31429  rfcnpre1  31561  rfcnpre2  31573  rfcnpre3  31575  rfcnpre4  31576  icccncfext  31856  ellkr  35227
  Copyright terms: Public domain W3C validator