Theorem elpreima 7006

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 6041	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3918	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6595	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2826	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 245	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6592	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7000	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 586	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 413	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 517	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7001	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6598	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 230	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 454	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 213	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  ^◡ccnv 5624  dom cdm 5625   “ cima 5628  Fun wfun 6486   Fn wfn 6487  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  elpreimad  7007  fniniseg  7008  fncnvima2  7009  unpreima  7011  respreima  7014  fnse  8080  brwitnlem  8439  unxpwdom2  9500  smobeth  10507  fpwwe2lem5  10556  hashkf  14292  isercolllem2  15626  isercolllem3  15627  isercoll  15628  fsumss  15685  fprodss  15911  tanval  16093  1arith  16896  0ram  16989  ghmpreima  19211  ghmnsgpreima  19214  kerf1ghm  19220  torsubg  19827  lmhmpreima  21045  rhmpreimaidl  21277  znunithash  21546  mpfind  22098  cncnpi  23268  cncnp  23270  cnpdis  23283  cnt0  23336  cnhaus  23344  2ndcomap  23448  1stccnp  23452  ptpjpre1  23561  tx1cn  23599  tx2cn  23600  txcnmpt  23614  txdis1cn  23625  hauseqlcld  23636  xkoptsub  23644  xkococn  23650  kqsat  23721  kqcldsat  23723  kqreglem1  23731  kqreglem2  23732  reghmph  23783  ordthmeolem  23791  tmdcn2  24079  clssubg  24099  tgphaus  24107  qustgplem  24111  ucncn  24274  xmeterval  24422  imasf1obl  24478  blval2  24552  metuel2  24555  isnghm  24713  cnbl0  24763  cnblcld  24764  cnheiborlem  24946  nmhmcn  25112  ismbl  25518  mbfeqalem1  25633  mbfmulc2lem  25639  mbfmax  25641  mbfposr  25644  mbfimaopnlem  25647  mbfaddlem  25652  mbfsup  25656  i1f1lem  25681  i1fpos  25698  mbfi1fseqlem4  25710  itg2monolem1  25742  itg2gt0  25752  itg2cnlem1  25753  itg2cnlem2  25754  plyeq0lem  26200  dgrlem  26219  dgrub  26224  dgrlb  26226  pserulm  26412  psercnlem2  26414  psercnlem1  26415  psercn  26416  abelth  26431  eff1olem  26537  ellogrn  26548  dvloglem  26637  logf1o2  26639  efopnlem1  26645  efopnlem2  26646  logtayl  26649  cxpcn3lem  26736  cxpcn3  26737  resqrtcn  26738  asinneg  26875  areambl  26947  sqff1o  27170  ubthlem1  30966  unipreima  32742  suppiniseg  32785  1stpreima  32806  2ndpreima  32807  suppss3  32822  hashgt1  32907  pwrssmgc  33086  tocyc01  33206  cyc3evpm  33238  elrgspnsubrunlem2  33336  kerunit  33415  elrspunidl  33518  rhmpreimaprmidl  33541  ply1degltel  33684  ply1degleel  33685  ply1degltdimlem  33813  irngnminplynz  33903  smatrcl  33987  rhmpreimacnlem  34075  cnre2csqlem  34101  elzrhunit  34168  qqhval2lem  34172  qqhf  34177  1stmbfm  34451  2ndmbfm  34452  mbfmcnt  34459  eulerpartlemsv2  34549  eulerpartlemv  34555  eulerpartlemf  34561  eulerpartlemgvv  34567  eulerpartlemgh  34569  eulerpartlemgs2  34571  sseqmw  34582  sseqf  34583  sseqp1  34586  fiblem  34589  fibp1  34592  cvmseu  35511  cvmliftmolem1  35516  cvmliftmolem2  35517  cvmliftlem15  35533  cvmlift2lem10  35547  cvmlift3lem8  35561  elmthm  35811  mthmblem  35815  mclsppslem  35818  mclspps  35819  cnambfre  38042  dvtan  38044  ftc1anclem3  38069  ftc1anclem5  38071  areacirc  38087  sstotbnd2  38148  keridl  38406  ellkr  39588  pw2f1ocnv  43489  binomcxplemdvbinom  44804  binomcxplemcvg  44805  binomcxplemnotnn0  44807  permaxpow  45460  rfcnpre1  45474  rfcnpre2  45486  rfcnpre3  45488  rfcnpre4  45489  limsupresxr  46216  liminfresxr  46217  icccncfext  46337  sge0fodjrnlem  46866  smfsuplem1  47261