Theorem elpreima 6997

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 6035	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3926	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6589	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2819	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6586	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6991	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6992	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6592	. . . 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 5618  dom cdm 5619   “ cima 5622  Fun wfun 6480   Fn wfn 6481  ‘cfv 6486

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 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-fv 6494

This theorem is referenced by:  elpreimad  6998  fniniseg  6999  fncnvima2  7000  unpreima  7002  respreima  7005  fnse  8069  brwitnlem  8428  unxpwdom2  9481  smobeth  10484  fpwwe2lem5  10533  hashkf  14241  isercolllem2  15575  isercolllem3  15576  isercoll  15577  fsumss  15634  fprodss  15857  tanval  16039  1arith  16841  0ram  16934  ghmpreima  19152  ghmnsgpreima  19155  kerf1ghm  19161  torsubg  19768  lmhmpreima  20984  rhmpreimaidl  21216  znunithash  21503  mpfind  22043  cncnpi  23194  cncnp  23196  cnpdis  23209  cnt0  23262  cnhaus  23270  2ndcomap  23374  1stccnp  23378  ptpjpre1  23487  tx1cn  23525  tx2cn  23526  txcnmpt  23540  txdis1cn  23551  hauseqlcld  23562  xkoptsub  23570  xkococn  23576  kqsat  23647  kqcldsat  23649  kqreglem1  23657  kqreglem2  23658  reghmph  23709  ordthmeolem  23717  tmdcn2  24005  clssubg  24025  tgphaus  24033  qustgplem  24037  ucncn  24200  xmeterval  24348  imasf1obl  24404  blval2  24478  metuel2  24481  isnghm  24639  cnbl0  24689  cnblcld  24690  cnheiborlem  24881  nmhmcn  25048  ismbl  25455  mbfeqalem1  25570  mbfmulc2lem  25576  mbfmax  25578  mbfposr  25581  mbfimaopnlem  25584  mbfaddlem  25589  mbfsup  25593  i1f1lem  25618  i1fpos  25635  mbfi1fseqlem4  25647  itg2monolem1  25679  itg2gt0  25689  itg2cnlem1  25690  itg2cnlem2  25691  plyeq0lem  26143  dgrlem  26162  dgrub  26167  dgrlb  26169  pserulm  26359  psercnlem2  26362  psercnlem1  26363  psercn  26364  abelth  26379  eff1olem  26485  ellogrn  26496  dvloglem  26585  logf1o2  26587  efopnlem1  26593  efopnlem2  26594  logtayl  26597  cxpcn3lem  26685  cxpcn3  26686  resqrtcn  26687  asinneg  26824  areambl  26896  sqff1o  27120  ubthlem1  30852  unipreima  32627  suppiniseg  32671  1stpreima  32692  2ndpreima  32693  suppss3  32710  hashgt1  32795  pwrssmgc  32988  tocyc01  33094  cyc3evpm  33126  elrgspnsubrunlem2  33222  kerunit  33297  elrspunidl  33400  rhmpreimaprmidl  33423  ply1degltel  33562  ply1degleel  33563  ply1degltdimlem  33656  irngnminplynz  33746  smatrcl  33830  rhmpreimacnlem  33918  cnre2csqlem  33944  elzrhunit  34011  qqhval2lem  34015  qqhf  34020  1stmbfm  34294  2ndmbfm  34295  mbfmcnt  34302  eulerpartlemsv2  34392  eulerpartlemv  34398  eulerpartlemf  34404  eulerpartlemgvv  34410  eulerpartlemgh  34412  eulerpartlemgs2  34414  sseqmw  34425  sseqf  34426  sseqp1  34429  fiblem  34432  fibp1  34435  cvmseu  35341  cvmliftmolem1  35346  cvmliftmolem2  35347  cvmliftlem15  35363  cvmlift2lem10  35377  cvmlift3lem8  35391  elmthm  35641  mthmblem  35645  mclsppslem  35648  mclspps  35649  cnambfre  37729  dvtan  37731  ftc1anclem3  37756  ftc1anclem5  37758  areacirc  37774  sstotbnd2  37835  keridl  38093  ellkr  39209  pw2f1ocnv  43155  binomcxplemdvbinom  44471  binomcxplemcvg  44472  binomcxplemnotnn0  44474  permaxpow  45127  rfcnpre1  45141  rfcnpre2  45153  rfcnpre3  45155  rfcnpre4  45156  limsupresxr  45889  liminfresxr  45890  icccncfext  46010  sge0fodjrnlem  46539  smfsuplem1  46934