Theorem elpreima 7057

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 6198	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3904	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6642	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2846	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 247	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6639	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7051	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 592	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 418	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 522	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7052	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6645	. . . 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 2144  ^◡ccnv 5649  dom cdm 5650   “ cima 5653  Fun wfun 6532   Fn wfn 6533  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546

This theorem is used by:  elpreimad  7058  fniniseg  7059  fncnvima2  7060  unpreima  7062  respreima  7065  fnse  8152  brwitnlem  8518  unxpwdom2  9585  smobeth  10674  fpwwe2lem5  10723  hashkf  14479  isercolllem2  15838  isercolllem3  15839  isercoll  15840  fsumss  15896  fprodss  16120  tanval  16301  1arith  17110  0ram  17203  ghmpreima  19457  ghmnsgpreima  19460  kerf1ghm  19466  torsubg  20073  lmhmpreima  21328  rhmpreimaidl  21576  rhmpreimaprmidl  21640  znunithash  21875  mpfind  22429  cncnpi  23601  cncnp  23603  cnpdis  23616  cnt0  23669  cnhaus  23677  2ndcomap  23782  1stccnp  23786  ptpjpre1  23895  tx1cn  23933  tx2cn  23934  txcnmpt  23948  txdis1cn  23959  hauseqlcld  23970  xkoptsub  23978  xkococn  23984  kqsat  24055  kqcldsat  24057  kqreglem1  24065  kqreglem2  24066  reghmph  24117  ordthmeolem  24125  tmdcn2  24413  clssubg  24433  tgphaus  24441  qustgplem  24445  ucncn  24608  xmeterval  24756  imasf1obl  24812  blval2  24886  metuel2  24889  isnghm  25047  cnbl0  25097  cnblcld  25098  cnheiborlem  25280  nmhmcn  25446  ismbl  25852  mbfeqalem1  25967  mbfmulc2lem  25973  mbfmax  25975  mbfposr  25978  mbfimaopnlem  25981  mbfaddlem  25986  mbfsup  25990  i1f1lem  26015  i1fpos  26032  mbfi1fseqlem4  26044  itg2monolem1  26076  itg2gt0  26086  itg2cnlem1  26087  itg2cnlem2  26088  plyeq0lem  26534  dgrlem  26553  dgrub  26558  dgrlb  26560  pserulm  26754  psercnlem2  26756  psercnlem1  26757  psercn  26758  abelth  26773  eff1olem  26881  ellogrn  26892  dvloglem  26981  logf1o2  26983  efopnlem1  26989  efopnlem2  26990  logtayl  26993  cxpcn3lem  27080  cxpcn3  27081  resqrtcn  27082  asinneg  27219  areambl  27291  sqff1o  27514  ubthlem1  31477  unipreima  33284  suppiniseg  33326  1stpreima  33347  2ndpreima  33348  suppss3  33361  hashgt1  33446  pwrssmgc  33607  tocyc01  33725  cyc3evpm  33757  elrgspnsubrunlem2  33855  kerunit  33932  elrspunidl  34024  ply1degltel  34172  ply1degleel  34173  ply1degltdimlem  34300  irngnminplynz  34390  smatrcl  34474  rhmpreimacnlem  34562  cnre2csqlem  34588  elzrhunit  34655  qqhval2lem  34659  qqhf  34664  1stmbfm  34938  2ndmbfm  34939  mbfmcnt  34946  eulerpartlemsv2  35036  eulerpartlemv  35042  eulerpartlemf  35048  eulerpartlemgvv  35054  eulerpartlemgh  35056  eulerpartlemgs2  35058  sseqmw  35069  sseqf  35070  sseqp1  35073  fiblem  35076  fibp1  35079  cvmseu  36127  cvmliftmolem1  36132  cvmliftmolem2  36133  cvmliftlem15  36149  cvmlift2lem10  36163  cvmlift3lem8  36177  elmthm  36427  mthmblem  36431  mclsppslem  36434  mclspps  36435  cnambfre  38679  dvtan  38681  ftc1anclem3  38706  ftc1anclem5  38708  areacirc  38724  sstotbnd2  38801  keridl  39059  ellkr  40239  pw2f1ocnv  44137  binomcxplemdvbinom  45430  binomcxplemcvg  45431  binomcxplemnotnn0  45433  permaxpow  46092  rfcnpre1  46129  rfcnpre2  46141  rfcnpre3  46143  rfcnpre4  46144  limsupresxr  46869  liminfresxr  46870  icccncfext  46990  sge0fodjrnlem  47519  smfsuplem1  47914