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

Theorem elpreima 5683
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 5070 . . . . 5  |-  ( `' F " C ) 
C_  dom  F
21sseli 3210 . . . 4  |-  ( B  e.  ( `' F " C )  ->  B  e.  dom  F )
3 fndm 5380 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2383 . . . 4  |-  ( F  Fn  A  ->  ( B  e.  dom  F  <->  B  e.  A ) )
52, 4syl5ib 210 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  ->  B  e.  A )
)
6 fnfun 5378 . . . . 5  |-  ( F  Fn  A  ->  Fun  F )
7 fvimacnvi 5677 . . . . 5  |-  ( ( Fun  F  /\  B  e.  ( `' F " C ) )  -> 
( F `  B
)  e.  C )
86, 7sylan 457 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  ( `' F " C ) )  ->  ( F `  B )  e.  C
)
98ex 423 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( F `  B
)  e.  C ) )
105, 9jcad 519 . 2  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( B  e.  A  /\  ( F `  B
)  e.  C ) ) )
11 fvimacnv 5678 . . . . 5  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1211funfni 5381 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1312biimpd 198 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  ->  B  e.  ( `' F " C ) ) )
1413expimpd 586 . 2  |-  ( F  Fn  A  ->  (
( B  e.  A  /\  ( F `  B
)  e.  C )  ->  B  e.  ( `' F " C ) ) )
1510, 14impbid 183 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 176    /\ wa 358    e. wcel 1701   `'ccnv 4725   dom cdm 4726   "cima 4729   Fun wfun 5286    Fn wfn 5287   ` cfv 5292
This theorem is referenced by:  fniniseg  5684  fncnvima2  5685  rexsupp  5688  unpreima  5689  respreima  5692  suppss  5696  suppssr  5697  fnse  6274  brwitnlem  6548  wemapso2  7312  unxpwdom2  7347  cantnfle  7417  cantnfp1lem2  7426  cantnfp1lem3  7427  cantnfp1  7428  oemapvali  7431  cantnflem1a  7432  cantnflem1c  7434  cantnflem3  7438  mapfien  7444  cnfcomlem  7447  cnfcom3  7452  smobeth  8253  fpwwe2lem6  8302  fpwwe2lem9  8305  hashkf  11386  isercolllem2  12186  isercolllem3  12187  isercoll  12188  fsumss  12245  tanval  12455  1arith  13021  0ram  13114  ghmpreima  14753  ghmnsgpreima  14756  torsubg  15195  lmhmpreima  15854  znunithash  16574  cncnpi  17063  cncnp  17065  cnpdis  17077  cnt0  17130  cnhaus  17138  2ndcomap  17240  1stccnp  17244  ptpjpre1  17322  tx1cn  17359  tx2cn  17360  txcnmpt  17374  txdis1cn  17385  hauseqlcld  17396  xkoptsub  17404  xkococn  17410  kqsat  17478  kqcldsat  17480  kqreglem1  17488  kqreglem2  17489  reghmph  17540  ordthmeolem  17548  tmdcn2  17824  clssubg  17843  tgphaus  17851  divstgplem  17855  xmeterval  18030  imasf1obl  18086  isnghm  18284  cnbl0  18335  cnblcld  18336  cnheiborlem  18505  nmhmcn  18654  ismbl  18938  mbfeqalem  19050  mbfmulc2lem  19055  mbfmax  19057  mbfposr  19060  mbfimaopnlem  19063  mbfaddlem  19068  mbfsup  19072  i1f1lem  19097  i1fpos  19114  mbfi1fseqlem4  19126  itg2monolem1  19158  itg2gt0  19168  itg2cnlem1  19169  itg2cnlem2  19170  evlslem3  19451  mpfind  19481  mdegleb  19503  plyeq0lem  19645  dgrlem  19664  dgrub  19669  dgrlb  19671  pserulm  19851  psercnlem2  19853  psercnlem1  19854  psercn  19855  abelth  19870  eff1olem  19963  ellogrn  19970  dvloglem  20048  logf1o2  20050  efopnlem1  20056  efopnlem2  20057  logtayl  20060  cxpcn3lem  20140  cxpcn3  20141  resqrcn  20142  asinneg  20235  areambl  20306  sqff1o  20473  ubthlem1  21504  unipreima  23205  1stpreima  23245  2ndpreima  23246  cnre2csqlem  23377  blval2  23506  kerunit  23541  kerf1hrm  23542  elzrhunit  23558  qqhval2lem  23560  qqhf  23565  1stmbfm  23784  2ndmbfm  23785  mbfmcnt  23792  cvmseu  24091  cvmliftmolem1  24096  cvmliftmolem2  24097  cvmliftlem15  24113  cvmlift2lem10  24127  cvmlift3lem8  24141  fprodss  24451  areacirc  25348  sstotbnd2  25646  keridl  25805  pw2f1ocnv  26278  rfcnpre1  26838  rfcnpre2  26850  rfcnpre3  26852  rfcnpre4  26853  ellkr  29097
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-fv 5300
  Copyright terms: Public domain W3C validator