Theorem elpreima 7012

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 6049	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3931	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6603	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2823	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6600	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7006	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 581	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7007	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6606	. . . 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 5631  dom cdm 5632   “ cima 5635  Fun wfun 6494   Fn wfn 6495  ‘cfv 6500

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 5243  ax-nul 5253  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-fv 6508

This theorem is referenced by:  elpreimad  7013  fniniseg  7014  fncnvima2  7015  unpreima  7017  respreima  7020  fnse  8085  brwitnlem  8444  unxpwdom2  9505  smobeth  10509  fpwwe2lem5  10558  hashkf  14267  isercolllem2  15601  isercolllem3  15602  isercoll  15603  fsumss  15660  fprodss  15883  tanval  16065  1arith  16867  0ram  16960  ghmpreima  19179  ghmnsgpreima  19182  kerf1ghm  19188  torsubg  19795  lmhmpreima  21012  rhmpreimaidl  21244  znunithash  21531  mpfind  22082  cncnpi  23234  cncnp  23236  cnpdis  23249  cnt0  23302  cnhaus  23310  2ndcomap  23414  1stccnp  23418  ptpjpre1  23527  tx1cn  23565  tx2cn  23566  txcnmpt  23580  txdis1cn  23591  hauseqlcld  23602  xkoptsub  23610  xkococn  23616  kqsat  23687  kqcldsat  23689  kqreglem1  23697  kqreglem2  23698  reghmph  23749  ordthmeolem  23757  tmdcn2  24045  clssubg  24065  tgphaus  24073  qustgplem  24077  ucncn  24240  xmeterval  24388  imasf1obl  24444  blval2  24518  metuel2  24521  isnghm  24679  cnbl0  24729  cnblcld  24730  cnheiborlem  24921  nmhmcn  25088  ismbl  25495  mbfeqalem1  25610  mbfmulc2lem  25616  mbfmax  25618  mbfposr  25621  mbfimaopnlem  25624  mbfaddlem  25629  mbfsup  25633  i1f1lem  25658  i1fpos  25675  mbfi1fseqlem4  25687  itg2monolem1  25719  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  plyeq0lem  26183  dgrlem  26202  dgrub  26207  dgrlb  26209  pserulm  26399  psercnlem2  26402  psercnlem1  26403  psercn  26404  abelth  26419  eff1olem  26525  ellogrn  26536  dvloglem  26625  logf1o2  26627  efopnlem1  26633  efopnlem2  26634  logtayl  26637  cxpcn3lem  26725  cxpcn3  26726  resqrtcn  26727  asinneg  26864  areambl  26936  sqff1o  27160  ubthlem1  30957  unipreima  32732  suppiniseg  32775  1stpreima  32796  2ndpreima  32797  suppss3  32812  hashgt1  32898  pwrssmgc  33092  tocyc01  33211  cyc3evpm  33243  elrgspnsubrunlem2  33341  kerunit  33417  elrspunidl  33520  rhmpreimaprmidl  33543  ply1degltel  33686  ply1degleel  33687  ply1degltdimlem  33799  irngnminplynz  33889  smatrcl  33973  rhmpreimacnlem  34061  cnre2csqlem  34087  elzrhunit  34154  qqhval2lem  34158  qqhf  34163  1stmbfm  34437  2ndmbfm  34438  mbfmcnt  34445  eulerpartlemsv2  34535  eulerpartlemv  34541  eulerpartlemf  34547  eulerpartlemgvv  34553  eulerpartlemgh  34555  eulerpartlemgs2  34557  sseqmw  34568  sseqf  34569  sseqp1  34572  fiblem  34575  fibp1  34578  cvmseu  35489  cvmliftmolem1  35494  cvmliftmolem2  35495  cvmliftlem15  35511  cvmlift2lem10  35525  cvmlift3lem8  35539  elmthm  35789  mthmblem  35793  mclsppslem  35796  mclspps  35797  cnambfre  37913  dvtan  37915  ftc1anclem3  37940  ftc1anclem5  37942  areacirc  37958  sstotbnd2  38019  keridl  38277  ellkr  39459  pw2f1ocnv  43388  binomcxplemdvbinom  44703  binomcxplemcvg  44704  binomcxplemnotnn0  44706  permaxpow  45359  rfcnpre1  45373  rfcnpre2  45385  rfcnpre3  45387  rfcnpre4  45388  limsupresxr  46118  liminfresxr  46119  icccncfext  46239  sge0fodjrnlem  46768  smfsuplem1  47163