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

Theorem elpreima 6323
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 5473 . . . . 5 (𝐹𝐶) ⊆ dom 𝐹
21sseli 3591 . . . 4 (𝐵 ∈ (𝐹𝐶) → 𝐵 ∈ dom 𝐹)
3 fndm 5978 . . . . 5 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2685 . . . 4 (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹𝐵𝐴))
52, 4syl5ib 234 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → 𝐵𝐴))
6 fnfun 5976 . . . . 5 (𝐹 Fn 𝐴 → Fun 𝐹)
7 fvimacnvi 6317 . . . . 5 ((Fun 𝐹𝐵 ∈ (𝐹𝐶)) → (𝐹𝐵) ∈ 𝐶)
86, 7sylan 488 . . . 4 ((𝐹 Fn 𝐴𝐵 ∈ (𝐹𝐶)) → (𝐹𝐵) ∈ 𝐶)
98ex 450 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → (𝐹𝐵) ∈ 𝐶))
105, 9jcad 555 . 2 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))
11 fvimacnv 6318 . . . . 5 ((Fun 𝐹𝐵 ∈ dom 𝐹) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1211funfni 5979 . . . 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 384  wcel 1988  ccnv 5103  dom cdm 5104  cima 5107  Fun wfun 5870   Fn wfn 5871  cfv 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-fv 5884
This theorem is referenced by:  fniniseg  6324  fncnvima2  6325  unpreima  6327  respreima  6330  fnse  7279  brwitnlem  7572  unxpwdom2  8478  smobeth  9393  fpwwe2lem6  9442  fpwwe2lem9  9445  hashkf  13102  isercolllem2  14377  isercolllem3  14378  isercoll  14379  fsumss  14437  fprodss  14659  tanval  14839  1arith  15612  0ram  15705  ghmpreima  17663  ghmnsgpreima  17666  torsubg  18238  kerf1hrm  18724  lmhmpreima  19029  evlslem3  19495  mpfind  19517  znunithash  19894  cncnpi  21063  cncnp  21065  cnpdis  21078  cnt0  21131  cnhaus  21139  2ndcomap  21242  1stccnp  21246  ptpjpre1  21355  tx1cn  21393  tx2cn  21394  txcnmpt  21408  txdis1cn  21419  hauseqlcld  21430  xkoptsub  21438  xkococn  21444  kqsat  21515  kqcldsat  21517  kqreglem1  21525  kqreglem2  21526  reghmph  21577  ordthmeolem  21585  tmdcn2  21874  clssubg  21893  tgphaus  21901  qustgplem  21905  ucncn  22070  xmeterval  22218  imasf1obl  22274  blval2  22348  metuel2  22351  isnghm  22508  cnbl0  22558  cnblcld  22559  cnheiborlem  22734  nmhmcn  22901  ismbl  23275  mbfeqalem  23390  mbfmulc2lem  23395  mbfmax  23397  mbfposr  23400  mbfimaopnlem  23403  mbfaddlem  23408  mbfsup  23412  i1f1lem  23437  i1fpos  23454  mbfi1fseqlem4  23466  itg2monolem1  23498  itg2gt0  23508  itg2cnlem1  23509  itg2cnlem2  23510  plyeq0lem  23947  dgrlem  23966  dgrub  23971  dgrlb  23973  pserulm  24157  psercnlem2  24159  psercnlem1  24160  psercn  24161  abelth  24176  eff1olem  24275  ellogrn  24287  dvloglem  24375  logf1o2  24377  efopnlem1  24383  efopnlem2  24384  logtayl  24387  cxpcn3lem  24469  cxpcn3  24470  resqrtcn  24471  asinneg  24594  areambl  24666  sqff1o  24889  ubthlem1  27696  unipreima  29419  1stpreima  29458  2ndpreima  29459  suppss3  29476  kerunit  29797  smatrcl  29836  cnre2csqlem  29930  elzrhunit  29997  qqhval2lem  29999  qqhf  30004  1stmbfm  30296  2ndmbfm  30297  mbfmcnt  30304  eulerpartlemsv2  30394  eulerpartlemv  30400  eulerpartlemf  30406  eulerpartlemgvv  30412  eulerpartlemgh  30414  eulerpartlemgs2  30416  sseqmw  30427  sseqf  30428  sseqp1  30431  fiblem  30434  fibp1  30437  cvmseu  31232  cvmliftmolem1  31237  cvmliftmolem2  31238  cvmliftlem15  31254  cvmlift2lem10  31268  cvmlift3lem8  31282  elmthm  31447  mthmblem  31451  mclsppslem  31454  mclspps  31455  cnambfre  33429  dvtan  33431  ftc1anclem3  33458  ftc1anclem5  33460  areacirc  33476  sstotbnd2  33544  keridl  33802  ellkr  34195  pw2f1ocnv  37423  binomcxplemdvbinom  38372  binomcxplemcvg  38373  binomcxplemnotnn0  38375  rfcnpre1  38998  rfcnpre2  39010  rfcnpre3  39012  rfcnpre4  39013  elpreimad  39270  limsupresxr  39792  liminfresxr  39793  icccncfext  39863  sge0fodjrnlem  40396  smfsuplem1  40780
  Copyright terms: Public domain W3C validator