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

Theorem elpreima 6559
Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
elpreima (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) ↔ (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))

Proof of Theorem elpreima
StepHypRef Expression
1 cnvimass 5695 . . . . 5 (𝐹𝐶) ⊆ dom 𝐹
21sseli 3794 . . . 4 (𝐵 ∈ (𝐹𝐶) → 𝐵 ∈ dom 𝐹)
3 fndm 6201 . . . . 5 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2871 . . . 4 (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹𝐵𝐴))
52, 4syl5ib 235 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → 𝐵𝐴))
6 fnfun 6199 . . . . 5 (𝐹 Fn 𝐴 → Fun 𝐹)
7 fvimacnvi 6553 . . . . 5 ((Fun 𝐹𝐵 ∈ (𝐹𝐶)) → (𝐹𝐵) ∈ 𝐶)
86, 7sylan 571 . . . 4 ((𝐹 Fn 𝐴𝐵 ∈ (𝐹𝐶)) → (𝐹𝐵) ∈ 𝐶)
98ex 399 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → (𝐹𝐵) ∈ 𝐶))
105, 9jcad 504 . 2 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))
11 fvimacnv 6554 . . . . 5 ((Fun 𝐹𝐵 ∈ dom 𝐹) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1211funfni 6202 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1312biimpd 220 . . 3 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1413expimpd 443 . 2 (𝐹 Fn 𝐴 → ((𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶) → 𝐵 ∈ (𝐹𝐶)))
1510, 14impbid 203 1 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) ↔ (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wcel 2156  ccnv 5310  dom cdm 5311  cima 5314  Fun wfun 6095   Fn wfn 6096  cfv 6101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-fv 6109
This theorem is referenced by:  fniniseg  6560  fncnvima2  6561  unpreima  6563  respreima  6566  fnse  7528  brwitnlem  7824  unxpwdom2  8732  smobeth  9693  fpwwe2lem6  9742  fpwwe2lem9  9745  hashkf  13339  isercolllem2  14619  isercolllem3  14620  isercoll  14621  fsumss  14679  fprodss  14899  tanval  15078  1arith  15848  0ram  15941  ghmpreima  17884  ghmnsgpreima  17887  torsubg  18458  kerf1hrm  18947  lmhmpreima  19255  evlslem3  19722  mpfind  19744  znunithash  20120  cncnpi  21296  cncnp  21298  cnpdis  21311  cnt0  21364  cnhaus  21372  2ndcomap  21475  1stccnp  21479  ptpjpre1  21588  tx1cn  21626  tx2cn  21627  txcnmpt  21641  txdis1cn  21652  hauseqlcld  21663  xkoptsub  21671  xkococn  21677  kqsat  21748  kqcldsat  21750  kqreglem1  21758  kqreglem2  21759  reghmph  21810  ordthmeolem  21818  tmdcn2  22106  clssubg  22125  tgphaus  22133  qustgplem  22137  ucncn  22302  xmeterval  22450  imasf1obl  22506  blval2  22580  metuel2  22583  isnghm  22740  cnbl0  22790  cnblcld  22791  cnheiborlem  22966  nmhmcn  23132  ismbl  23507  mbfeqalem1  23622  mbfmulc2lem  23628  mbfmax  23630  mbfposr  23633  mbfimaopnlem  23636  mbfaddlem  23641  mbfsup  23645  i1f1lem  23670  i1fpos  23687  mbfi1fseqlem4  23699  itg2monolem1  23731  itg2gt0  23741  itg2cnlem1  23742  itg2cnlem2  23743  plyeq0lem  24180  dgrlem  24199  dgrub  24204  dgrlb  24206  pserulm  24390  psercnlem2  24392  psercnlem1  24393  psercn  24394  abelth  24409  eff1olem  24509  ellogrn  24520  dvloglem  24608  logf1o2  24610  efopnlem1  24616  efopnlem2  24617  logtayl  24620  cxpcn3lem  24702  cxpcn3  24703  resqrtcn  24704  asinneg  24827  areambl  24899  sqff1o  25122  ubthlem1  28054  unipreima  29773  1stpreima  29811  2ndpreima  29812  suppss3  29829  kerunit  30148  smatrcl  30187  cnre2csqlem  30281  elzrhunit  30348  qqhval2lem  30350  qqhf  30355  1stmbfm  30647  2ndmbfm  30648  mbfmcnt  30655  eulerpartlemsv2  30745  eulerpartlemv  30751  eulerpartlemf  30757  eulerpartlemgvv  30763  eulerpartlemgh  30765  eulerpartlemgs2  30767  sseqmw  30778  sseqf  30779  sseqp1  30782  fiblem  30785  fibp1  30788  cvmseu  31581  cvmliftmolem1  31586  cvmliftmolem2  31587  cvmliftlem15  31603  cvmlift2lem10  31617  cvmlift3lem8  31631  elmthm  31796  mthmblem  31800  mclsppslem  31803  mclspps  31804  cnambfre  33770  dvtan  33772  ftc1anclem3  33799  ftc1anclem5  33801  areacirc  33817  sstotbnd2  33884  keridl  34142  ellkr  34869  pw2f1ocnv  38105  binomcxplemdvbinom  39052  binomcxplemcvg  39053  binomcxplemnotnn0  39055  rfcnpre1  39672  rfcnpre2  39684  rfcnpre3  39686  rfcnpre4  39687  elpreimad  39938  limsupresxr  40478  liminfresxr  40479  icccncfext  40580  sge0fodjrnlem  41112  smfsuplem1  41499
  Copyright terms: Public domain W3C validator