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

Theorem elpreima 6377
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 5520 . . . . 5 (𝐹𝐶) ⊆ dom 𝐹
21sseli 3632 . . . 4 (𝐵 ∈ (𝐹𝐶) → 𝐵 ∈ dom 𝐹)
3 fndm 6028 . . . . 5 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2716 . . . 4 (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹𝐵𝐴))
52, 4syl5ib 234 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → 𝐵𝐴))
6 fnfun 6026 . . . . 5 (𝐹 Fn 𝐴 → Fun 𝐹)
7 fvimacnvi 6371 . . . . 5 ((Fun 𝐹𝐵 ∈ (𝐹𝐶)) → (𝐹𝐵) ∈ 𝐶)
86, 7sylan 487 . . . 4 ((𝐹 Fn 𝐴𝐵 ∈ (𝐹𝐶)) → (𝐹𝐵) ∈ 𝐶)
98ex 449 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → (𝐹𝐵) ∈ 𝐶))
105, 9jcad 554 . 2 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))
11 fvimacnv 6372 . . . . 5 ((Fun 𝐹𝐵 ∈ dom 𝐹) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1211funfni 6029 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1312biimpd 219 . . 3 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1413expimpd 628 . 2 (𝐹 Fn 𝐴 → ((𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶) → 𝐵 ∈ (𝐹𝐶)))
1510, 14impbid 202 1 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) ↔ (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2030  ccnv 5142  dom cdm 5143  cima 5146  Fun wfun 5920   Fn wfn 5921  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-fv 5934
This theorem is referenced by:  fniniseg  6378  fncnvima2  6379  unpreima  6381  respreima  6384  fnse  7339  brwitnlem  7632  unxpwdom2  8534  smobeth  9446  fpwwe2lem6  9495  fpwwe2lem9  9498  hashkf  13159  isercolllem2  14440  isercolllem3  14441  isercoll  14442  fsumss  14500  fprodss  14722  tanval  14902  1arith  15678  0ram  15771  ghmpreima  17729  ghmnsgpreima  17732  torsubg  18303  kerf1hrm  18791  lmhmpreima  19096  evlslem3  19562  mpfind  19584  znunithash  19961  cncnpi  21130  cncnp  21132  cnpdis  21145  cnt0  21198  cnhaus  21206  2ndcomap  21309  1stccnp  21313  ptpjpre1  21422  tx1cn  21460  tx2cn  21461  txcnmpt  21475  txdis1cn  21486  hauseqlcld  21497  xkoptsub  21505  xkococn  21511  kqsat  21582  kqcldsat  21584  kqreglem1  21592  kqreglem2  21593  reghmph  21644  ordthmeolem  21652  tmdcn2  21940  clssubg  21959  tgphaus  21967  qustgplem  21971  ucncn  22136  xmeterval  22284  imasf1obl  22340  blval2  22414  metuel2  22417  isnghm  22574  cnbl0  22624  cnblcld  22625  cnheiborlem  22800  nmhmcn  22966  ismbl  23340  mbfeqalem  23454  mbfmulc2lem  23459  mbfmax  23461  mbfposr  23464  mbfimaopnlem  23467  mbfaddlem  23472  mbfsup  23476  i1f1lem  23501  i1fpos  23518  mbfi1fseqlem4  23530  itg2monolem1  23562  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  plyeq0lem  24011  dgrlem  24030  dgrub  24035  dgrlb  24037  pserulm  24221  psercnlem2  24223  psercnlem1  24224  psercn  24225  abelth  24240  eff1olem  24339  ellogrn  24351  dvloglem  24439  logf1o2  24441  efopnlem1  24447  efopnlem2  24448  logtayl  24451  cxpcn3lem  24533  cxpcn3  24534  resqrtcn  24535  asinneg  24658  areambl  24730  sqff1o  24953  ubthlem1  27854  unipreima  29574  1stpreima  29612  2ndpreima  29613  suppss3  29630  kerunit  29951  smatrcl  29990  cnre2csqlem  30084  elzrhunit  30151  qqhval2lem  30153  qqhf  30158  1stmbfm  30450  2ndmbfm  30451  mbfmcnt  30458  eulerpartlemsv2  30548  eulerpartlemv  30554  eulerpartlemf  30560  eulerpartlemgvv  30566  eulerpartlemgh  30568  eulerpartlemgs2  30570  sseqmw  30581  sseqf  30582  sseqp1  30585  fiblem  30588  fibp1  30591  cvmseu  31384  cvmliftmolem1  31389  cvmliftmolem2  31390  cvmliftlem15  31406  cvmlift2lem10  31420  cvmlift3lem8  31434  elmthm  31599  mthmblem  31603  mclsppslem  31606  mclspps  31607  cnambfre  33588  dvtan  33590  ftc1anclem3  33617  ftc1anclem5  33619  areacirc  33635  sstotbnd2  33703  keridl  33961  ellkr  34694  pw2f1ocnv  37921  binomcxplemdvbinom  38869  binomcxplemcvg  38870  binomcxplemnotnn0  38872  rfcnpre1  39492  rfcnpre2  39504  rfcnpre3  39506  rfcnpre4  39507  elpreimad  39768  limsupresxr  40316  liminfresxr  40317  icccncfext  40418  sge0fodjrnlem  40951  smfsuplem1  41338
  Copyright terms: Public domain W3C validator