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 4584  df-pr 4586  df-op 4590  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  8150  brwitnlem  8515  unxpwdom2  9582  smobeth  10671  fpwwe2lem5  10720  hashkf  14476  isercolllem2  15833  isercolllem3  15834  isercoll  15835  fsumss  15891  fprodss  16115  tanval  16296  1arith  17105  0ram  17198  ghmpreima  19452  ghmnsgpreima  19455  kerf1ghm  19461  torsubg  20068  lmhmpreima  21323  rhmpreimaidl  21571  rhmpreimaprmidl  21635  znunithash  21870  mpfind  22424  cncnpi  23596  cncnp  23598  cnpdis  23611  cnt0  23664  cnhaus  23672  2ndcomap  23777  1stccnp  23781  ptpjpre1  23890  tx1cn  23928  tx2cn  23929  txcnmpt  23943  txdis1cn  23954  hauseqlcld  23965  xkoptsub  23973  xkococn  23979  kqsat  24050  kqcldsat  24052  kqreglem1  24060  kqreglem2  24061  reghmph  24112  ordthmeolem  24120  tmdcn2  24408  clssubg  24428  tgphaus  24436  qustgplem  24440  ucncn  24603  xmeterval  24751  imasf1obl  24807  blval2  24881  metuel2  24884  isnghm  25042  cnbl0  25092  cnblcld  25093  cnheiborlem  25275  nmhmcn  25441  ismbl  25847  mbfeqalem1  25962  mbfmulc2lem  25968  mbfmax  25970  mbfposr  25973  mbfimaopnlem  25976  mbfaddlem  25981  mbfsup  25985  i1f1lem  26010  i1fpos  26027  mbfi1fseqlem4  26039  itg2monolem1  26071  itg2gt0  26081  itg2cnlem1  26082  itg2cnlem2  26083  plyeq0lem  26529  dgrlem  26548  dgrub  26553  dgrlb  26555  pserulm  26749  psercnlem2  26751  psercnlem1  26752  psercn  26753  abelth  26768  eff1olem  26876  ellogrn  26887  dvloglem  26976  logf1o2  26978  efopnlem1  26984  efopnlem2  26985  logtayl  26988  cxpcn3lem  27075  cxpcn3  27076  resqrtcn  27077  asinneg  27214  areambl  27286  sqff1o  27509  ubthlem1  31472  unipreima  33237  suppiniseg  33279  1stpreima  33300  2ndpreima  33301  suppss3  33315  hashgt1  33400  pwrssmgc  33561  tocyc01  33679  cyc3evpm  33711  elrgspnsubrunlem2  33809  kerunit  33886  elrspunidl  33978  ply1degltel  34126  ply1degleel  34127  ply1degltdimlem  34254  irngnminplynz  34344  smatrcl  34428  rhmpreimacnlem  34516  cnre2csqlem  34542  elzrhunit  34609  qqhval2lem  34613  qqhf  34618  1stmbfm  34892  2ndmbfm  34893  mbfmcnt  34900  eulerpartlemsv2  34990  eulerpartlemv  34996  eulerpartlemf  35002  eulerpartlemgvv  35008  eulerpartlemgh  35010  eulerpartlemgs2  35012  sseqmw  35023  sseqf  35024  sseqp1  35027  fiblem  35030  fibp1  35033  cvmseu  36041  cvmliftmolem1  36046  cvmliftmolem2  36047  cvmliftlem15  36063  cvmlift2lem10  36077  cvmlift3lem8  36091  elmthm  36341  mthmblem  36345  mclsppslem  36348  mclspps  36349  cnambfre  38587  dvtan  38589  ftc1anclem3  38614  ftc1anclem5  38616  areacirc  38632  sstotbnd2  38709  keridl  38967  ellkr  40147  pw2f1ocnv  44044  binomcxplemdvbinom  45337  binomcxplemcvg  45338  binomcxplemnotnn0  45340  permaxpow  45999  rfcnpre1  46036  rfcnpre2  46048  rfcnpre3  46050  rfcnpre4  46051  limsupresxr  46776  liminfresxr  46777  icccncfext  46897  sge0fodjrnlem  47426  smfsuplem1  47821