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

Theorem elpreima 5852
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 5226 . . . . 5  |-  ( `' F " C ) 
C_  dom  F
21sseli 3346 . . . 4  |-  ( B  e.  ( `' F " C )  ->  B  e.  dom  F )
3 fndm 5546 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2505 . . . 4  |-  ( F  Fn  A  ->  ( B  e.  dom  F  <->  B  e.  A ) )
52, 4syl5ib 212 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  ->  B  e.  A )
)
6 fnfun 5544 . . . . 5  |-  ( F  Fn  A  ->  Fun  F )
7 fvimacnvi 5846 . . . . 5  |-  ( ( Fun  F  /\  B  e.  ( `' F " C ) )  -> 
( F `  B
)  e.  C )
86, 7sylan 459 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  ( `' F " C ) )  ->  ( F `  B )  e.  C
)
98ex 425 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( F `  B
)  e.  C ) )
105, 9jcad 521 . 2  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( B  e.  A  /\  ( F `  B
)  e.  C ) ) )
11 fvimacnv 5847 . . . . 5  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1211funfni 5547 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1312biimpd 200 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  ->  B  e.  ( `' F " C ) ) )
1413expimpd 588 . 2  |-  ( F  Fn  A  ->  (
( B  e.  A  /\  ( F `  B
)  e.  C )  ->  B  e.  ( `' F " C ) ) )
1510, 14impbid 185 1  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  <->  ( B  e.  A  /\  ( F `  B )  e.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    e. wcel 1726   `'ccnv 4879   dom cdm 4880   "cima 4883   Fun wfun 5450    Fn wfn 5451   ` cfv 5456
This theorem is referenced by:  fniniseg  5853  fncnvima2  5854  rexsupp  5857  unpreima  5858  respreima  5861  suppss  5865  suppssr  5866  fnse  6465  brwitnlem  6753  wemapso2  7523  unxpwdom2  7558  cantnfle  7628  cantnfp1lem2  7637  cantnfp1lem3  7638  cantnfp1  7639  oemapvali  7642  cantnflem1a  7643  cantnflem1c  7645  cantnflem3  7649  mapfien  7655  cnfcomlem  7658  cnfcom3  7663  smobeth  8463  fpwwe2lem6  8512  fpwwe2lem9  8515  hashkf  11622  isercolllem2  12461  isercolllem3  12462  isercoll  12463  fsumss  12521  tanval  12731  1arith  13297  0ram  13390  ghmpreima  15029  ghmnsgpreima  15032  torsubg  15471  lmhmpreima  16126  znunithash  16847  cncnpi  17344  cncnp  17346  cnpdis  17359  cnt0  17412  cnhaus  17420  2ndcomap  17523  1stccnp  17527  ptpjpre1  17605  tx1cn  17643  tx2cn  17644  txcnmpt  17658  txdis1cn  17669  hauseqlcld  17680  xkoptsub  17688  xkococn  17694  kqsat  17765  kqcldsat  17767  kqreglem1  17775  kqreglem2  17776  reghmph  17827  ordthmeolem  17835  tmdcn2  18121  clssubg  18140  tgphaus  18148  divstgplem  18152  ucncn  18317  xmeterval  18464  imasf1obl  18520  blval2  18607  metuel2  18611  isnghm  18759  cnbl0  18810  cnblcld  18811  cnheiborlem  18981  nmhmcn  19130  ismbl  19424  mbfeqalem  19536  mbfmulc2lem  19541  mbfmax  19543  mbfposr  19546  mbfimaopnlem  19549  mbfaddlem  19554  mbfsup  19558  i1f1lem  19583  i1fpos  19600  mbfi1fseqlem4  19612  itg2monolem1  19644  itg2gt0  19654  itg2cnlem1  19655  itg2cnlem2  19656  evlslem3  19937  mpfind  19967  mdegleb  19989  plyeq0lem  20131  dgrlem  20150  dgrub  20155  dgrlb  20157  pserulm  20340  psercnlem2  20342  psercnlem1  20343  psercn  20344  abelth  20359  eff1olem  20452  ellogrn  20459  dvloglem  20541  logf1o2  20543  efopnlem1  20549  efopnlem2  20550  logtayl  20553  cxpcn3lem  20633  cxpcn3  20634  resqrcn  20635  asinneg  20728  areambl  20799  sqff1o  20967  ubthlem1  22374  unipreima  24058  1stpreima  24097  2ndpreima  24098  kerunit  24263  kerf1hrm  24264  cnre2csqlem  24310  elzrhunit  24365  qqhval2lem  24367  qqhf  24372  1stmbfm  24612  2ndmbfm  24613  mbfmcnt  24620  cvmseu  24965  cvmliftmolem1  24970  cvmliftmolem2  24971  cvmliftlem15  24987  cvmlift2lem10  25001  cvmlift3lem8  25015  fprodss  25276  cnambfre  26257  ftc1anclem3  26284  ftc1anclem5  26286  areacirc  26299  sstotbnd2  26485  keridl  26644  pw2f1ocnv  27110  rfcnpre1  27668  rfcnpre2  27680  rfcnpre3  27682  rfcnpre4  27683  ellkr  29949
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-fv 5464
  Copyright terms: Public domain W3C validator