Theorem elpreima 7060

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 6089	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3936	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6645	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2852	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 247	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6642	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7054	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 592	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 418	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 522	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7055	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6648	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 232	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 459	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 215	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  ^◡ccnv 5665  dom cdm 5666   “ cima 5669  Fun wfun 6537   Fn wfn 6538  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-fv 6551

This theorem is used by:  elpreimad  7061  fniniseg  7062  fncnvima2  7063  unpreima  7065  respreima  7068  fnse  8138  brwitnlem  8501  unxpwdom2  9560  smobeth  10589  fpwwe2lem5  10638  hashkf  14388  isercolllem2  15743  isercolllem3  15744  isercoll  15745  fsumss  15802  fprodss  16028  tanval  16209  1arith  17012  0ram  17105  ghmpreima  19339  ghmnsgpreima  19342  kerf1ghm  19348  torsubg  19955  lmhmpreima  21206  rhmpreimaidl  21453  rhmpreimaprmidl  21516  znunithash  21751  mpfind  22303  cncnpi  23472  cncnp  23474  cnpdis  23487  cnt0  23540  cnhaus  23548  2ndcomap  23652  1stccnp  23656  ptpjpre1  23765  tx1cn  23803  tx2cn  23804  txcnmpt  23818  txdis1cn  23829  hauseqlcld  23840  xkoptsub  23848  xkococn  23854  kqsat  23925  kqcldsat  23927  kqreglem1  23935  kqreglem2  23936  reghmph  23987  ordthmeolem  23995  tmdcn2  24283  clssubg  24303  tgphaus  24311  qustgplem  24315  ucncn  24478  xmeterval  24626  imasf1obl  24682  blval2  24756  metuel2  24759  isnghm  24917  cnbl0  24967  cnblcld  24968  cnheiborlem  25150  nmhmcn  25316  ismbl  25722  mbfeqalem1  25837  mbfmulc2lem  25843  mbfmax  25845  mbfposr  25848  mbfimaopnlem  25851  mbfaddlem  25856  mbfsup  25860  i1f1lem  25885  i1fpos  25902  mbfi1fseqlem4  25914  itg2monolem1  25946  itg2gt0  25956  itg2cnlem1  25957  itg2cnlem2  25958  plyeq0lem  26404  dgrlem  26423  dgrub  26428  dgrlb  26430  pserulm  26622  psercnlem2  26624  psercnlem1  26625  psercn  26626  abelth  26641  eff1olem  26750  ellogrn  26761  dvloglem  26850  logf1o2  26852  efopnlem1  26858  efopnlem2  26859  logtayl  26862  cxpcn3lem  26949  cxpcn3  26950  resqrtcn  26951  asinneg  27088  areambl  27160  sqff1o  27383  ubthlem1  31259  unipreima  33025  suppiniseg  33068  1stpreima  33089  2ndpreima  33090  suppss3  33105  hashgt1  33190  pwrssmgc  33351  tocyc01  33469  cyc3evpm  33501  elrgspnsubrunlem2  33599  kerunit  33676  elrspunidl  33767  ply1degltel  33915  ply1degleel  33916  ply1degltdimlem  34043  irngnminplynz  34133  smatrcl  34217  rhmpreimacnlem  34305  cnre2csqlem  34331  elzrhunit  34398  qqhval2lem  34402  qqhf  34407  1stmbfm  34682  2ndmbfm  34683  mbfmcnt  34690  eulerpartlemsv2  34780  eulerpartlemv  34786  eulerpartlemf  34792  eulerpartlemgvv  34798  eulerpartlemgh  34800  eulerpartlemgs2  34802  sseqmw  34813  sseqf  34814  sseqp1  34817  fiblem  34820  fibp1  34823  cvmseu  35789  cvmliftmolem1  35794  cvmliftmolem2  35795  cvmliftlem15  35811  cvmlift2lem10  35825  cvmlift3lem8  35839  elmthm  36089  mthmblem  36093  mclsppslem  36096  mclspps  36097  cnambfre  38360  dvtan  38362  ftc1anclem3  38387  ftc1anclem5  38389  areacirc  38405  sstotbnd2  38466  keridl  38724  ellkr  39904  pw2f1ocnv  43805  binomcxplemdvbinom  45104  binomcxplemcvg  45105  binomcxplemnotnn0  45107  permaxpow  45759  rfcnpre1  45780  rfcnpre2  45792  rfcnpre3  45794  rfcnpre4  45795  limsupresxr  46521  liminfresxr  46522  icccncfext  46642  sge0fodjrnlem  47171  smfsuplem1  47566