Theorem elpreima 6944

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 5992	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3918	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6545	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2825	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	syl5ib 243	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6542	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6938	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 413	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 513	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6939	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6548	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 228	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 454	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 211	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2107  ^◡ccnv 5589  dom cdm 5590   “ cima 5593  Fun wfun 6431   Fn wfn 6432  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-fv 6445

This theorem is referenced by:  elpreimad  6945  fniniseg  6946  fncnvima2  6947  unpreima  6949  respreima  6952  fnse  7983  brwitnlem  8346  unxpwdom2  9356  smobeth  10351  fpwwe2lem5  10400  hashkf  14055  isercolllem2  15386  isercolllem3  15387  isercoll  15388  fsumss  15446  fprodss  15667  tanval  15846  1arith  16637  0ram  16730  ghmpreima  18865  ghmnsgpreima  18868  torsubg  19464  kerf1ghm  19996  lmhmpreima  20319  znunithash  20781  mpfind  21326  cncnpi  22438  cncnp  22440  cnpdis  22453  cnt0  22506  cnhaus  22514  2ndcomap  22618  1stccnp  22622  ptpjpre1  22731  tx1cn  22769  tx2cn  22770  txcnmpt  22784  txdis1cn  22795  hauseqlcld  22806  xkoptsub  22814  xkococn  22820  kqsat  22891  kqcldsat  22893  kqreglem1  22901  kqreglem2  22902  reghmph  22953  ordthmeolem  22961  tmdcn2  23249  clssubg  23269  tgphaus  23277  qustgplem  23281  ucncn  23446  xmeterval  23594  imasf1obl  23653  blval2  23727  metuel2  23730  isnghm  23896  cnbl0  23946  cnblcld  23947  cnheiborlem  24126  nmhmcn  24292  ismbl  24699  mbfeqalem1  24814  mbfmulc2lem  24820  mbfmax  24822  mbfposr  24825  mbfimaopnlem  24828  mbfaddlem  24833  mbfsup  24837  i1f1lem  24862  i1fpos  24880  mbfi1fseqlem4  24892  itg2monolem1  24924  itg2gt0  24934  itg2cnlem1  24935  itg2cnlem2  24936  plyeq0lem  25380  dgrlem  25399  dgrub  25404  dgrlb  25406  pserulm  25590  psercnlem2  25592  psercnlem1  25593  psercn  25594  abelth  25609  eff1olem  25713  ellogrn  25724  dvloglem  25812  logf1o2  25814  efopnlem1  25820  efopnlem2  25821  logtayl  25824  cxpcn3lem  25909  cxpcn3  25910  resqrtcn  25911  asinneg  26045  areambl  26117  sqff1o  26340  ubthlem1  29241  unipreima  30990  suppiniseg  31029  1stpreima  31048  2ndpreima  31049  suppss3  31068  hashgt1  31137  pwrssmgc  31287  tocyc01  31394  cyc3evpm  31426  kerunit  31531  rhmpreimaidl  31612  elrspunidl  31615  rhmpreimaprmidl  31636  smatrcl  31755  rhmpreimacnlem  31843  cnre2csqlem  31869  elzrhunit  31938  qqhval2lem  31940  qqhf  31945  1stmbfm  32236  2ndmbfm  32237  mbfmcnt  32244  eulerpartlemsv2  32334  eulerpartlemv  32340  eulerpartlemf  32346  eulerpartlemgvv  32352  eulerpartlemgh  32354  eulerpartlemgs2  32356  sseqmw  32367  sseqf  32368  sseqp1  32371  fiblem  32374  fibp1  32377  cvmseu  33247  cvmliftmolem1  33252  cvmliftmolem2  33253  cvmliftlem15  33269  cvmlift2lem10  33283  cvmlift3lem8  33297  elmthm  33547  mthmblem  33551  mclsppslem  33554  mclspps  33555  cnambfre  35834  dvtan  35836  ftc1anclem3  35861  ftc1anclem5  35863  areacirc  35879  sstotbnd2  35941  keridl  36199  ellkr  37110  pw2f1ocnv  40866  binomcxplemdvbinom  41978  binomcxplemcvg  41979  binomcxplemnotnn0  41981  rfcnpre1  42569  rfcnpre2  42581  rfcnpre3  42583  rfcnpre4  42584  limsupresxr  43314  liminfresxr  43315  icccncfext  43435  sge0fodjrnlem  43961  smfsuplem1  44355