Theorem elpreima 7003

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 3929	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6595	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2822	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6592	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6997	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6998	. . . . 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 2113  ^◡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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  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  7004  fniniseg  7005  fncnvima2  7006  unpreima  7008  respreima  7011  fnse  8075  brwitnlem  8434  unxpwdom2  9493  smobeth  10497  fpwwe2lem5  10546  hashkf  14255  isercolllem2  15589  isercolllem3  15590  isercoll  15591  fsumss  15648  fprodss  15871  tanval  16053  1arith  16855  0ram  16948  ghmpreima  19167  ghmnsgpreima  19170  kerf1ghm  19176  torsubg  19783  lmhmpreima  21000  rhmpreimaidl  21232  znunithash  21519  mpfind  22070  cncnpi  23222  cncnp  23224  cnpdis  23237  cnt0  23290  cnhaus  23298  2ndcomap  23402  1stccnp  23406  ptpjpre1  23515  tx1cn  23553  tx2cn  23554  txcnmpt  23568  txdis1cn  23579  hauseqlcld  23590  xkoptsub  23598  xkococn  23604  kqsat  23675  kqcldsat  23677  kqreglem1  23685  kqreglem2  23686  reghmph  23737  ordthmeolem  23745  tmdcn2  24033  clssubg  24053  tgphaus  24061  qustgplem  24065  ucncn  24228  xmeterval  24376  imasf1obl  24432  blval2  24506  metuel2  24509  isnghm  24667  cnbl0  24717  cnblcld  24718  cnheiborlem  24909  nmhmcn  25076  ismbl  25483  mbfeqalem1  25598  mbfmulc2lem  25604  mbfmax  25606  mbfposr  25609  mbfimaopnlem  25612  mbfaddlem  25617  mbfsup  25621  i1f1lem  25646  i1fpos  25663  mbfi1fseqlem4  25675  itg2monolem1  25707  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  plyeq0lem  26171  dgrlem  26190  dgrub  26195  dgrlb  26197  pserulm  26387  psercnlem2  26390  psercnlem1  26391  psercn  26392  abelth  26407  eff1olem  26513  ellogrn  26524  dvloglem  26613  logf1o2  26615  efopnlem1  26621  efopnlem2  26622  logtayl  26625  cxpcn3lem  26713  cxpcn3  26714  resqrtcn  26715  asinneg  26852  areambl  26924  sqff1o  27148  ubthlem1  30945  unipreima  32721  suppiniseg  32765  1stpreima  32786  2ndpreima  32787  suppss3  32802  hashgt1  32888  pwrssmgc  33082  tocyc01  33200  cyc3evpm  33232  elrgspnsubrunlem2  33330  kerunit  33406  elrspunidl  33509  rhmpreimaprmidl  33532  ply1degltel  33675  ply1degleel  33676  ply1degltdimlem  33779  irngnminplynz  33869  smatrcl  33953  rhmpreimacnlem  34041  cnre2csqlem  34067  elzrhunit  34134  qqhval2lem  34138  qqhf  34143  1stmbfm  34417  2ndmbfm  34418  mbfmcnt  34425  eulerpartlemsv2  34515  eulerpartlemv  34521  eulerpartlemf  34527  eulerpartlemgvv  34533  eulerpartlemgh  34535  eulerpartlemgs2  34537  sseqmw  34548  sseqf  34549  sseqp1  34552  fiblem  34555  fibp1  34558  cvmseu  35470  cvmliftmolem1  35475  cvmliftmolem2  35476  cvmliftlem15  35492  cvmlift2lem10  35506  cvmlift3lem8  35520  elmthm  35770  mthmblem  35774  mclsppslem  35777  mclspps  35778  cnambfre  37865  dvtan  37867  ftc1anclem3  37892  ftc1anclem5  37894  areacirc  37910  sstotbnd2  37971  keridl  38229  ellkr  39345  pw2f1ocnv  43275  binomcxplemdvbinom  44590  binomcxplemcvg  44591  binomcxplemnotnn0  44593  permaxpow  45246  rfcnpre1  45260  rfcnpre2  45272  rfcnpre3  45274  rfcnpre4  45275  limsupresxr  46006  liminfresxr  46007  icccncfext  46127  sge0fodjrnlem  46656  smfsuplem1  47051