Theorem elpreima 6837

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 5923	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3873	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6440	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2818	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	syl5ib 247	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6438	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6831	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 583	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 416	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 516	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6832	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6443	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 232	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 457	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 215	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2114  ^◡ccnv 5524  dom cdm 5525   “ cima 5528  Fun wfun 6333   Fn wfn 6334  ‘cfv 6339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fn 6342  df-fv 6347

This theorem is referenced by:  elpreimad  6838  fniniseg  6839  fncnvima2  6840  unpreima  6842  respreima  6845  fnse  7855  brwitnlem  8165  unxpwdom2  9127  smobeth  10088  fpwwe2lem5  10137  hashkf  13786  isercolllem2  15117  isercolllem3  15118  isercoll  15119  fsumss  15177  fprodss  15396  tanval  15575  1arith  16365  0ram  16458  ghmpreima  18500  ghmnsgpreima  18503  torsubg  19095  kerf1ghm  19619  lmhmpreima  19941  znunithash  20385  mpfind  20923  cncnpi  22031  cncnp  22033  cnpdis  22046  cnt0  22099  cnhaus  22107  2ndcomap  22211  1stccnp  22215  ptpjpre1  22324  tx1cn  22362  tx2cn  22363  txcnmpt  22377  txdis1cn  22388  hauseqlcld  22399  xkoptsub  22407  xkococn  22413  kqsat  22484  kqcldsat  22486  kqreglem1  22494  kqreglem2  22495  reghmph  22546  ordthmeolem  22554  tmdcn2  22842  clssubg  22862  tgphaus  22870  qustgplem  22874  ucncn  23039  xmeterval  23187  imasf1obl  23243  blval2  23317  metuel2  23320  isnghm  23478  cnbl0  23528  cnblcld  23529  cnheiborlem  23708  nmhmcn  23874  ismbl  24280  mbfeqalem1  24395  mbfmulc2lem  24401  mbfmax  24403  mbfposr  24406  mbfimaopnlem  24409  mbfaddlem  24414  mbfsup  24418  i1f1lem  24443  i1fpos  24461  mbfi1fseqlem4  24473  itg2monolem1  24505  itg2gt0  24515  itg2cnlem1  24516  itg2cnlem2  24517  plyeq0lem  24961  dgrlem  24980  dgrub  24985  dgrlb  24987  pserulm  25171  psercnlem2  25173  psercnlem1  25174  psercn  25175  abelth  25190  eff1olem  25294  ellogrn  25305  dvloglem  25393  logf1o2  25395  efopnlem1  25401  efopnlem2  25402  logtayl  25405  cxpcn3lem  25490  cxpcn3  25491  resqrtcn  25492  asinneg  25626  areambl  25698  sqff1o  25921  ubthlem1  28807  unipreima  30557  suppiniseg  30597  1stpreima  30616  2ndpreima  30617  suppss3  30636  hashgt1  30705  pwrssmgc  30857  tocyc01  30964  cyc3evpm  30996  kerunit  31101  rhmpreimaidl  31177  elrspunidl  31180  rhmpreimaprmidl  31201  smatrcl  31320  rhmpreimacnlem  31408  cnre2csqlem  31434  elzrhunit  31501  qqhval2lem  31503  qqhf  31508  1stmbfm  31799  2ndmbfm  31800  mbfmcnt  31807  eulerpartlemsv2  31897  eulerpartlemv  31903  eulerpartlemf  31909  eulerpartlemgvv  31915  eulerpartlemgh  31917  eulerpartlemgs2  31919  sseqmw  31930  sseqf  31931  sseqp1  31934  fiblem  31937  fibp1  31940  cvmseu  32811  cvmliftmolem1  32816  cvmliftmolem2  32817  cvmliftlem15  32833  cvmlift2lem10  32847  cvmlift3lem8  32861  elmthm  33111  mthmblem  33115  mclsppslem  33118  mclspps  33119  cnambfre  35470  dvtan  35472  ftc1anclem3  35497  ftc1anclem5  35499  areacirc  35515  sstotbnd2  35577  keridl  35835  ellkr  36748  pw2f1ocnv  40453  binomcxplemdvbinom  41531  binomcxplemcvg  41532  binomcxplemnotnn0  41534  rfcnpre1  42122  rfcnpre2  42134  rfcnpre3  42136  rfcnpre4  42137  limsupresxr  42871  liminfresxr  42872  icccncfext  42992  sge0fodjrnlem  43518  smfsuplem1  43905