Theorem elpreima 6917

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

Step	Hyp	Ref	Expression
1		cnvimass 5978	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3913	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6520	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2824	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	syl5ib 243	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6517	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6911	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 579	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6912	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6523	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 228	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 453	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 211	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  ^◡ccnv 5579  dom cdm 5580   “ cima 5583  Fun wfun 6412   Fn wfn 6413  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-fv 6426

This theorem is referenced by:  elpreimad  6918  fniniseg  6919  fncnvima2  6920  unpreima  6922  respreima  6925  fnse  7945  brwitnlem  8299  unxpwdom2  9277  smobeth  10273  fpwwe2lem5  10322  hashkf  13974  isercolllem2  15305  isercolllem3  15306  isercoll  15307  fsumss  15365  fprodss  15586  tanval  15765  1arith  16556  0ram  16649  ghmpreima  18771  ghmnsgpreima  18774  torsubg  19370  kerf1ghm  19902  lmhmpreima  20225  znunithash  20684  mpfind  21227  cncnpi  22337  cncnp  22339  cnpdis  22352  cnt0  22405  cnhaus  22413  2ndcomap  22517  1stccnp  22521  ptpjpre1  22630  tx1cn  22668  tx2cn  22669  txcnmpt  22683  txdis1cn  22694  hauseqlcld  22705  xkoptsub  22713  xkococn  22719  kqsat  22790  kqcldsat  22792  kqreglem1  22800  kqreglem2  22801  reghmph  22852  ordthmeolem  22860  tmdcn2  23148  clssubg  23168  tgphaus  23176  qustgplem  23180  ucncn  23345  xmeterval  23493  imasf1obl  23550  blval2  23624  metuel2  23627  isnghm  23793  cnbl0  23843  cnblcld  23844  cnheiborlem  24023  nmhmcn  24189  ismbl  24595  mbfeqalem1  24710  mbfmulc2lem  24716  mbfmax  24718  mbfposr  24721  mbfimaopnlem  24724  mbfaddlem  24729  mbfsup  24733  i1f1lem  24758  i1fpos  24776  mbfi1fseqlem4  24788  itg2monolem1  24820  itg2gt0  24830  itg2cnlem1  24831  itg2cnlem2  24832  plyeq0lem  25276  dgrlem  25295  dgrub  25300  dgrlb  25302  pserulm  25486  psercnlem2  25488  psercnlem1  25489  psercn  25490  abelth  25505  eff1olem  25609  ellogrn  25620  dvloglem  25708  logf1o2  25710  efopnlem1  25716  efopnlem2  25717  logtayl  25720  cxpcn3lem  25805  cxpcn3  25806  resqrtcn  25807  asinneg  25941  areambl  26013  sqff1o  26236  ubthlem1  29133  unipreima  30882  suppiniseg  30922  1stpreima  30941  2ndpreima  30942  suppss3  30961  hashgt1  31030  pwrssmgc  31180  tocyc01  31287  cyc3evpm  31319  kerunit  31424  rhmpreimaidl  31505  elrspunidl  31508  rhmpreimaprmidl  31529  smatrcl  31648  rhmpreimacnlem  31736  cnre2csqlem  31762  elzrhunit  31829  qqhval2lem  31831  qqhf  31836  1stmbfm  32127  2ndmbfm  32128  mbfmcnt  32135  eulerpartlemsv2  32225  eulerpartlemv  32231  eulerpartlemf  32237  eulerpartlemgvv  32243  eulerpartlemgh  32245  eulerpartlemgs2  32247  sseqmw  32258  sseqf  32259  sseqp1  32262  fiblem  32265  fibp1  32268  cvmseu  33138  cvmliftmolem1  33143  cvmliftmolem2  33144  cvmliftlem15  33160  cvmlift2lem10  33174  cvmlift3lem8  33188  elmthm  33438  mthmblem  33442  mclsppslem  33445  mclspps  33446  cnambfre  35752  dvtan  35754  ftc1anclem3  35779  ftc1anclem5  35781  areacirc  35797  sstotbnd2  35859  keridl  36117  ellkr  37030  pw2f1ocnv  40775  binomcxplemdvbinom  41860  binomcxplemcvg  41861  binomcxplemnotnn0  41863  rfcnpre1  42451  rfcnpre2  42463  rfcnpre3  42465  rfcnpre4  42466  limsupresxr  43197  liminfresxr  43198  icccncfext  43318  sge0fodjrnlem  43844  smfsuplem1  44231