Theorem elpreima 6827

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 5948	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3962	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6454	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2898	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	syl5ib 246	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6452	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6821	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 582	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 415	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 515	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6822	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6456	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 231	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 456	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 214	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2110  ^◡ccnv 5553  dom cdm 5554   “ cima 5557  Fun wfun 6348   Fn wfn 6349  ‘cfv 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-fv 6362

This theorem is referenced by:  elpreimad  6828  fniniseg  6829  fncnvima2  6830  unpreima  6832  respreima  6835  fnse  7826  brwitnlem  8131  unxpwdom2  9051  smobeth  10007  fpwwe2lem6  10056  fpwwe2lem9  10059  hashkf  13691  isercolllem2  15021  isercolllem3  15022  isercoll  15023  fsumss  15081  fprodss  15301  tanval  15480  1arith  16262  0ram  16355  ghmpreima  18379  ghmnsgpreima  18382  torsubg  18973  kerf1ghm  19496  kerf1hrmOLD  19497  lmhmpreima  19819  mpfind  20319  znunithash  20710  cncnpi  21885  cncnp  21887  cnpdis  21900  cnt0  21953  cnhaus  21961  2ndcomap  22065  1stccnp  22069  ptpjpre1  22178  tx1cn  22216  tx2cn  22217  txcnmpt  22231  txdis1cn  22242  hauseqlcld  22253  xkoptsub  22261  xkococn  22267  kqsat  22338  kqcldsat  22340  kqreglem1  22348  kqreglem2  22349  reghmph  22400  ordthmeolem  22408  tmdcn2  22696  clssubg  22716  tgphaus  22724  qustgplem  22728  ucncn  22893  xmeterval  23041  imasf1obl  23097  blval2  23171  metuel2  23174  isnghm  23331  cnbl0  23381  cnblcld  23382  cnheiborlem  23557  nmhmcn  23723  ismbl  24126  mbfeqalem1  24241  mbfmulc2lem  24247  mbfmax  24249  mbfposr  24252  mbfimaopnlem  24255  mbfaddlem  24260  mbfsup  24264  i1f1lem  24289  i1fpos  24306  mbfi1fseqlem4  24318  itg2monolem1  24350  itg2gt0  24360  itg2cnlem1  24361  itg2cnlem2  24362  plyeq0lem  24799  dgrlem  24818  dgrub  24823  dgrlb  24825  pserulm  25009  psercnlem2  25011  psercnlem1  25012  psercn  25013  abelth  25028  eff1olem  25131  ellogrn  25142  dvloglem  25230  logf1o2  25232  efopnlem1  25238  efopnlem2  25239  logtayl  25242  cxpcn3lem  25327  cxpcn3  25328  resqrtcn  25329  asinneg  25463  areambl  25535  sqff1o  25758  ubthlem1  28646  unipreima  30390  1stpreima  30441  2ndpreima  30442  suppss3  30459  hashgt1  30529  tocyc01  30760  cyc3evpm  30792  kerunit  30896  smatrcl  31061  cnre2csqlem  31153  elzrhunit  31220  qqhval2lem  31222  qqhf  31227  1stmbfm  31518  2ndmbfm  31519  mbfmcnt  31526  eulerpartlemsv2  31616  eulerpartlemv  31622  eulerpartlemf  31628  eulerpartlemgvv  31634  eulerpartlemgh  31636  eulerpartlemgs2  31638  sseqmw  31649  sseqf  31650  sseqp1  31653  fiblem  31656  fibp1  31659  cvmseu  32523  cvmliftmolem1  32528  cvmliftmolem2  32529  cvmliftlem15  32545  cvmlift2lem10  32559  cvmlift3lem8  32573  elmthm  32823  mthmblem  32827  mclsppslem  32830  mclspps  32831  cnambfre  34939  dvtan  34941  ftc1anclem3  34968  ftc1anclem5  34970  areacirc  34986  sstotbnd2  35051  keridl  35309  ellkr  36224  pw2f1ocnv  39632  binomcxplemdvbinom  40683  binomcxplemcvg  40684  binomcxplemnotnn0  40686  rfcnpre1  41274  rfcnpre2  41286  rfcnpre3  41288  rfcnpre4  41289  limsupresxr  42045  liminfresxr  42046  icccncfext  42168  sge0fodjrnlem  42697  smfsuplem1  43084