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 6081	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3979	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6653	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2820	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 243	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6650	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7054	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 581	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 414	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 514	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7055	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6656	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 228	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 455	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 211	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  ^◡ccnv 5676  dom cdm 5677   “ cima 5680  Fun wfun 6538   Fn wfn 6539  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-fv 6552

This theorem is referenced by:  elpreimad  7061  fniniseg  7062  fncnvima2  7063  unpreima  7065  respreima  7068  fnse  8119  brwitnlem  8507  unxpwdom2  9583  smobeth  10581  fpwwe2lem5  10630  hashkf  14292  isercolllem2  15612  isercolllem3  15613  isercoll  15614  fsumss  15671  fprodss  15892  tanval  16071  1arith  16860  0ram  16953  ghmpreima  19114  ghmnsgpreima  19117  torsubg  19722  kerf1ghm  20282  lmhmpreima  20659  znunithash  21120  mpfind  21670  cncnpi  22782  cncnp  22784  cnpdis  22797  cnt0  22850  cnhaus  22858  2ndcomap  22962  1stccnp  22966  ptpjpre1  23075  tx1cn  23113  tx2cn  23114  txcnmpt  23128  txdis1cn  23139  hauseqlcld  23150  xkoptsub  23158  xkococn  23164  kqsat  23235  kqcldsat  23237  kqreglem1  23245  kqreglem2  23246  reghmph  23297  ordthmeolem  23305  tmdcn2  23593  clssubg  23613  tgphaus  23621  qustgplem  23625  ucncn  23790  xmeterval  23938  imasf1obl  23997  blval2  24071  metuel2  24074  isnghm  24240  cnbl0  24290  cnblcld  24291  cnheiborlem  24470  nmhmcn  24636  ismbl  25043  mbfeqalem1  25158  mbfmulc2lem  25164  mbfmax  25166  mbfposr  25169  mbfimaopnlem  25172  mbfaddlem  25177  mbfsup  25181  i1f1lem  25206  i1fpos  25224  mbfi1fseqlem4  25236  itg2monolem1  25268  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  plyeq0lem  25724  dgrlem  25743  dgrub  25748  dgrlb  25750  pserulm  25934  psercnlem2  25936  psercnlem1  25937  psercn  25938  abelth  25953  eff1olem  26057  ellogrn  26068  dvloglem  26156  logf1o2  26158  efopnlem1  26164  efopnlem2  26165  logtayl  26168  cxpcn3lem  26255  cxpcn3  26256  resqrtcn  26257  asinneg  26391  areambl  26463  sqff1o  26686  ubthlem1  30123  unipreima  31869  suppiniseg  31908  1stpreima  31928  2ndpreima  31929  suppss3  31949  hashgt1  32020  pwrssmgc  32170  tocyc01  32277  cyc3evpm  32309  kerunit  32437  rhmpreimaidl  32537  elrspunidl  32546  rhmpreimaprmidl  32570  ply1degltel  32666  ply1degltdimlem  32707  irngnminplynz  32771  smatrcl  32776  rhmpreimacnlem  32864  cnre2csqlem  32890  elzrhunit  32959  qqhval2lem  32961  qqhf  32966  1stmbfm  33259  2ndmbfm  33260  mbfmcnt  33267  eulerpartlemsv2  33357  eulerpartlemv  33363  eulerpartlemf  33369  eulerpartlemgvv  33375  eulerpartlemgh  33377  eulerpartlemgs2  33379  sseqmw  33390  sseqf  33391  sseqp1  33394  fiblem  33397  fibp1  33400  cvmseu  34267  cvmliftmolem1  34272  cvmliftmolem2  34273  cvmliftlem15  34289  cvmlift2lem10  34303  cvmlift3lem8  34317  elmthm  34567  mthmblem  34571  mclsppslem  34574  mclspps  34575  cnambfre  36536  dvtan  36538  ftc1anclem3  36563  ftc1anclem5  36565  areacirc  36581  sstotbnd2  36642  keridl  36900  ellkr  37959  pw2f1ocnv  41776  binomcxplemdvbinom  43112  binomcxplemcvg  43113  binomcxplemnotnn0  43115  rfcnpre1  43703  rfcnpre2  43715  rfcnpre3  43717  rfcnpre4  43718  limsupresxr  44482  liminfresxr  44483  icccncfext  44603  sge0fodjrnlem  45132  smfsuplem1  45527