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

Theorem elpreima 5816
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 5182 . . . . 5  |-  ( `' F " C ) 
C_  dom  F
21sseli 3345 . . . 4  |-  ( B  e.  ( `' F " C )  ->  B  e.  dom  F )
3 fndm 5503 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2504 . . . 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 5501 . . . . 5  |-  ( F  Fn  A  ->  Fun  F )
7 fvimacnvi 5810 . . . . 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 5811 . . . . 5  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1211funfni 5504 . . . 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 4831   dom cdm 4832   "cima 4835   Fun wfun 5405    Fn wfn 5406   ` cfv 5411
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 2418  ax-sep 4406  ax-nul 4414  ax-pr 4524
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 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-fv 5419
This theorem is referenced by:  fniniseg  5817  fncnvima2  5818  rexsuppOLD  5821  unpreima  5822  respreima  5825  suppssOLD  5829  suppssrOLD  5830  fnse  6684  brwitnlem  6939  wemapso2OLD  7758  unxpwdom2  7795  cantnfleOLD  7901  cantnfp1lem2OLD  7905  cantnfp1lem3OLD  7906  cantnfp1OLD  7907  cantnflem1aOLD  7908  cantnflem1cOLD  7910  cantnflem3OLD  7913  mapfienOLD  7919  cnfcomlemOLD  7932  cnfcom3OLD  7937  smobeth  8742  fpwwe2lem6  8794  fpwwe2lem9  8797  hashkf  12097  isercolllem2  13135  isercolllem3  13136  isercoll  13137  fsumss  13194  tanval  13404  1arith  13980  0ram  14073  ghmpreima  15757  ghmnsgpreima  15760  torsubg  16325  lmhmpreima  17103  evlslem3  17572  mpfind  17594  znunithash  17966  cncnpi  18851  cncnp  18853  cnpdis  18866  cnt0  18919  cnhaus  18927  2ndcomap  19031  1stccnp  19035  ptpjpre1  19113  tx1cn  19151  tx2cn  19152  txcnmpt  19166  txdis1cn  19177  hauseqlcld  19188  xkoptsub  19196  xkococn  19202  kqsat  19273  kqcldsat  19275  kqreglem1  19283  kqreglem2  19284  reghmph  19335  ordthmeolem  19343  tmdcn2  19629  clssubg  19648  tgphaus  19656  divstgplem  19660  ucncn  19829  xmeterval  19976  imasf1obl  20032  blval2  20119  metuel2  20123  isnghm  20271  cnbl0  20322  cnblcld  20323  cnheiborlem  20495  nmhmcn  20644  ismbl  20978  mbfeqalem  21089  mbfmulc2lem  21094  mbfmax  21096  mbfposr  21099  mbfimaopnlem  21102  mbfaddlem  21107  mbfsup  21111  i1f1lem  21136  i1fpos  21153  mbfi1fseqlem4  21165  itg2monolem1  21197  itg2gt0  21207  itg2cnlem1  21208  itg2cnlem2  21209  plyeq0lem  21647  dgrlem  21666  dgrub  21671  dgrlb  21673  pserulm  21856  psercnlem2  21858  psercnlem1  21859  psercn  21860  abelth  21875  eff1olem  21973  ellogrn  21980  dvloglem  22062  logf1o2  22064  efopnlem1  22070  efopnlem2  22071  logtayl  22074  cxpcn3lem  22154  cxpcn3  22155  resqrcn  22156  asinneg  22250  areambl  22321  sqff1o  22489  ubthlem1  24216  unipreima  25906  1stpreima  25946  2ndpreima  25947  suppss3  25972  kerunit  26238  kerf1hrm  26239  cnre2csqlem  26288  elzrhunit  26356  qqhval2lem  26358  qqhf  26363  1stmbfm  26623  2ndmbfm  26624  mbfmcnt  26631  eulerpartlemsv2  26689  eulerpartlemv  26695  eulerpartlemf  26701  eulerpartlemgvv  26707  eulerpartlemgh  26709  eulerpartlemgs2  26711  sseqmw  26722  sseqf  26723  sseqp1  26726  fiblem  26729  fibp1  26732  cvmseu  27113  cvmliftmolem1  27118  cvmliftmolem2  27119  cvmliftlem15  27135  cvmlift2lem10  27149  cvmlift3lem8  27163  fprodss  27408  cnambfre  28383  dvtan  28385  ftc1anclem3  28412  ftc1anclem5  28414  areacirc  28432  sstotbnd2  28616  keridl  28775  pw2f1ocnv  29329  rfcnpre1  29684  rfcnpre2  29696  rfcnpre3  29698  rfcnpre4  29699  ellkr  32485
  Copyright terms: Public domain W3C validator