Theorem elpreima 7004

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 2823	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6592	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6998	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 581	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6999	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6598	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 229	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 453	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 212	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ^◡ccnv 5623  dom cdm 5624   “ cima 5627  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  elpreimad  7005  fniniseg  7006  fncnvima2  7007  unpreima  7009  respreima  7012  fnse  8076  brwitnlem  8435  unxpwdom2  9496  smobeth  10500  fpwwe2lem5  10549  hashkf  14285  isercolllem2  15619  isercolllem3  15620  isercoll  15621  fsumss  15678  fprodss  15904  tanval  16086  1arith  16889  0ram  16982  ghmpreima  19204  ghmnsgpreima  19207  kerf1ghm  19213  torsubg  19820  lmhmpreima  21035  rhmpreimaidl  21267  znunithash  21554  mpfind  22103  cncnpi  23253  cncnp  23255  cnpdis  23268  cnt0  23321  cnhaus  23329  2ndcomap  23433  1stccnp  23437  ptpjpre1  23546  tx1cn  23584  tx2cn  23585  txcnmpt  23599  txdis1cn  23610  hauseqlcld  23621  xkoptsub  23629  xkococn  23635  kqsat  23706  kqcldsat  23708  kqreglem1  23716  kqreglem2  23717  reghmph  23768  ordthmeolem  23776  tmdcn2  24064  clssubg  24084  tgphaus  24092  qustgplem  24096  ucncn  24259  xmeterval  24407  imasf1obl  24463  blval2  24537  metuel2  24540  isnghm  24698  cnbl0  24748  cnblcld  24749  cnheiborlem  24931  nmhmcn  25097  ismbl  25503  mbfeqalem1  25618  mbfmulc2lem  25624  mbfmax  25626  mbfposr  25629  mbfimaopnlem  25632  mbfaddlem  25637  mbfsup  25641  i1f1lem  25666  i1fpos  25683  mbfi1fseqlem4  25695  itg2monolem1  25727  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  plyeq0lem  26185  dgrlem  26204  dgrub  26209  dgrlb  26211  pserulm  26400  psercnlem2  26402  psercnlem1  26403  psercn  26404  abelth  26419  eff1olem  26525  ellogrn  26536  dvloglem  26625  logf1o2  26627  efopnlem1  26633  efopnlem2  26634  logtayl  26637  cxpcn3lem  26724  cxpcn3  26725  resqrtcn  26726  asinneg  26863  areambl  26935  sqff1o  27159  ubthlem1  30956  unipreima  32731  suppiniseg  32774  1stpreima  32795  2ndpreima  32796  suppss3  32811  hashgt1  32896  pwrssmgc  33075  tocyc01  33194  cyc3evpm  33226  elrgspnsubrunlem2  33324  kerunit  33400  elrspunidl  33503  rhmpreimaprmidl  33526  ply1degltel  33669  ply1degleel  33670  ply1degltdimlem  33782  irngnminplynz  33872  smatrcl  33956  rhmpreimacnlem  34044  cnre2csqlem  34070  elzrhunit  34137  qqhval2lem  34141  qqhf  34146  1stmbfm  34420  2ndmbfm  34421  mbfmcnt  34428  eulerpartlemsv2  34518  eulerpartlemv  34524  eulerpartlemf  34530  eulerpartlemgvv  34536  eulerpartlemgh  34538  eulerpartlemgs2  34540  sseqmw  34551  sseqf  34552  sseqp1  34555  fiblem  34558  fibp1  34561  cvmseu  35474  cvmliftmolem1  35479  cvmliftmolem2  35480  cvmliftlem15  35496  cvmlift2lem10  35510  cvmlift3lem8  35524  elmthm  35774  mthmblem  35778  mclsppslem  35781  mclspps  35782  cnambfre  38003  dvtan  38005  ftc1anclem3  38030  ftc1anclem5  38032  areacirc  38048  sstotbnd2  38109  keridl  38367  ellkr  39549  pw2f1ocnv  43483  binomcxplemdvbinom  44798  binomcxplemcvg  44799  binomcxplemnotnn0  44801  permaxpow  45454  rfcnpre1  45468  rfcnpre2  45480  rfcnpre3  45482  rfcnpre4  45483  limsupresxr  46212  liminfresxr  46213  icccncfext  46333  sge0fodjrnlem  46862  smfsuplem1  47257