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

Theorem elpreima 6007
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 5191 . . . . 5  |-  ( `' F " C ) 
C_  dom  F
21sseli 3430 . . . 4  |-  ( B  e.  ( `' F " C )  ->  B  e.  dom  F )
3 fndm 5680 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2516 . . . 4  |-  ( F  Fn  A  ->  ( B  e.  dom  F  <->  B  e.  A ) )
52, 4syl5ib 223 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  ->  B  e.  A )
)
6 fnfun 5678 . . . . 5  |-  ( F  Fn  A  ->  Fun  F )
7 fvimacnvi 6001 . . . . 5  |-  ( ( Fun  F  /\  B  e.  ( `' F " C ) )  -> 
( F `  B
)  e.  C )
86, 7sylan 474 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  ( `' F " C ) )  ->  ( F `  B )  e.  C
)
98ex 436 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( F `  B
)  e.  C ) )
105, 9jcad 536 . 2  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( B  e.  A  /\  ( F `  B
)  e.  C ) ) )
11 fvimacnv 6002 . . . . 5  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1211funfni 5681 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1312biimpd 211 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  ->  B  e.  ( `' F " C ) ) )
1413expimpd 608 . 2  |-  ( F  Fn  A  ->  (
( B  e.  A  /\  ( F `  B
)  e.  C )  ->  B  e.  ( `' F " C ) ) )
1510, 14impbid 194 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 188    /\ wa 371    e. wcel 1889   `'ccnv 4836   dom cdm 4837   "cima 4840   Fun wfun 5579    Fn wfn 5580   ` cfv 5585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-fv 5593
This theorem is referenced by:  fniniseg  6008  fncnvima2  6009  unpreima  6011  respreima  6014  fnse  6918  brwitnlem  7214  unxpwdom2  8108  smobeth  9016  fpwwe2lem6  9065  fpwwe2lem9  9068  hashkf  12524  isercolllem2  13741  isercolllem3  13742  isercoll  13743  fsumss  13803  fprodss  14014  tanval  14194  1arith  14883  0ram  14990  ghmpreima  16916  ghmnsgpreima  16919  torsubg  17504  kerf1hrm  17983  lmhmpreima  18283  evlslem3  18749  mpfind  18771  znunithash  19147  cncnpi  20306  cncnp  20308  cnpdis  20321  cnt0  20374  cnhaus  20382  2ndcomap  20485  1stccnp  20489  ptpjpre1  20598  tx1cn  20636  tx2cn  20637  txcnmpt  20651  txdis1cn  20662  hauseqlcld  20673  xkoptsub  20681  xkococn  20687  kqsat  20758  kqcldsat  20760  kqreglem1  20768  kqreglem2  20769  reghmph  20820  ordthmeolem  20828  tmdcn2  21116  clssubg  21135  tgphaus  21143  qustgplem  21147  ucncn  21312  xmeterval  21459  imasf1obl  21515  blval2  21589  metuel2  21592  isnghm  21740  isnghmOLD  21758  cnbl0  21806  cnblcld  21807  cnheiborlem  21994  nmhmcn  22146  ismbl  22492  mbfeqalem  22610  mbfmulc2lem  22615  mbfmax  22617  mbfposr  22620  mbfimaopnlem  22623  mbfaddlem  22628  mbfsup  22632  i1f1lem  22659  i1fpos  22676  mbfi1fseqlem4  22688  itg2monolem1  22720  itg2gt0  22730  itg2cnlem1  22731  itg2cnlem2  22732  plyeq0lem  23176  dgrlem  23195  dgrub  23200  dgrlb  23202  pserulm  23389  psercnlem2  23391  psercnlem1  23392  psercn  23393  abelth  23408  eff1olem  23509  ellogrn  23521  dvloglem  23605  logf1o2  23607  efopnlem1  23613  efopnlem2  23614  logtayl  23617  cxpcn3lem  23699  cxpcn3  23700  resqrtcn  23701  asinneg  23824  areambl  23896  sqff1o  24121  ubthlem1  26524  unipreima  28257  1stpreima  28299  2ndpreima  28300  suppss3  28324  kerunit  28598  smatrcl  28634  cnre2csqlem  28728  elzrhunit  28795  qqhval2lem  28797  qqhf  28802  1stmbfm  29094  2ndmbfm  29095  mbfmcnt  29102  eulerpartlemsv2  29203  eulerpartlemv  29209  eulerpartlemf  29215  eulerpartlemgvv  29221  eulerpartlemgh  29223  eulerpartlemgs2  29225  sseqmw  29236  sseqf  29237  sseqp1  29240  fiblem  29243  fibp1  29246  cvmseu  30011  cvmliftmolem1  30016  cvmliftmolem2  30017  cvmliftlem15  30033  cvmlift2lem10  30047  cvmlift3lem8  30061  elmthm  30226  mthmblem  30230  mclsppslem  30233  mclspps  30234  cnambfre  32001  dvtan  32004  ftc1anclem3  32031  ftc1anclem5  32033  areacirc  32049  sstotbnd2  32118  keridl  32277  ellkr  32667  pw2f1ocnv  35904  binomcxplemdvbinom  36713  binomcxplemcvg  36714  binomcxplemnotnn0  36716  rfcnpre1  37350  rfcnpre2  37362  rfcnpre3  37364  rfcnpre4  37365  icccncfext  37775  sge0fodjrnlem  38268
  Copyright terms: Public domain W3C validator