Theorem elpreima 6337

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 5485	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3599	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 5990	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2687	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	syl5ib 234	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 5988	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6331	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 488	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 450	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 555	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6332	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 5991	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 219	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 629	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 202	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∈ wcel 1990  ^◡ccnv 5113  dom cdm 5114   “ cima 5117  Fun wfun 5882   Fn wfn 5883  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896

This theorem is referenced by:  fniniseg  6338  fncnvima2  6339  unpreima  6341  respreima  6344  fnse  7294  brwitnlem  7587  unxpwdom2  8493  smobeth  9408  fpwwe2lem6  9457  fpwwe2lem9  9460  hashkf  13119  isercolllem2  14396  isercolllem3  14397  isercoll  14398  fsumss  14456  fprodss  14678  tanval  14858  1arith  15631  0ram  15724  ghmpreima  17682  ghmnsgpreima  17685  torsubg  18257  kerf1hrm  18743  lmhmpreima  19048  evlslem3  19514  mpfind  19536  znunithash  19913  cncnpi  21082  cncnp  21084  cnpdis  21097  cnt0  21150  cnhaus  21158  2ndcomap  21261  1stccnp  21265  ptpjpre1  21374  tx1cn  21412  tx2cn  21413  txcnmpt  21427  txdis1cn  21438  hauseqlcld  21449  xkoptsub  21457  xkococn  21463  kqsat  21534  kqcldsat  21536  kqreglem1  21544  kqreglem2  21545  reghmph  21596  ordthmeolem  21604  tmdcn2  21893  clssubg  21912  tgphaus  21920  qustgplem  21924  ucncn  22089  xmeterval  22237  imasf1obl  22293  blval2  22367  metuel2  22370  isnghm  22527  cnbl0  22577  cnblcld  22578  cnheiborlem  22753  nmhmcn  22920  ismbl  23294  mbfeqalem  23409  mbfmulc2lem  23414  mbfmax  23416  mbfposr  23419  mbfimaopnlem  23422  mbfaddlem  23427  mbfsup  23431  i1f1lem  23456  i1fpos  23473  mbfi1fseqlem4  23485  itg2monolem1  23517  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  plyeq0lem  23966  dgrlem  23985  dgrub  23990  dgrlb  23992  pserulm  24176  psercnlem2  24178  psercnlem1  24179  psercn  24180  abelth  24195  eff1olem  24294  ellogrn  24306  dvloglem  24394  logf1o2  24396  efopnlem1  24402  efopnlem2  24403  logtayl  24406  cxpcn3lem  24488  cxpcn3  24489  resqrtcn  24490  asinneg  24613  areambl  24685  sqff1o  24908  ubthlem1  27726  unipreima  29446  1stpreima  29484  2ndpreima  29485  suppss3  29502  kerunit  29823  smatrcl  29862  cnre2csqlem  29956  elzrhunit  30023  qqhval2lem  30025  qqhf  30030  1stmbfm  30322  2ndmbfm  30323  mbfmcnt  30330  eulerpartlemsv2  30420  eulerpartlemv  30426  eulerpartlemf  30432  eulerpartlemgvv  30438  eulerpartlemgh  30440  eulerpartlemgs2  30442  sseqmw  30453  sseqf  30454  sseqp1  30457  fiblem  30460  fibp1  30463  cvmseu  31258  cvmliftmolem1  31263  cvmliftmolem2  31264  cvmliftlem15  31280  cvmlift2lem10  31294  cvmlift3lem8  31308  elmthm  31473  mthmblem  31477  mclsppslem  31480  mclspps  31481  cnambfre  33458  dvtan  33460  ftc1anclem3  33487  ftc1anclem5  33489  areacirc  33505  sstotbnd2  33573  keridl  33831  ellkr  34376  pw2f1ocnv  37604  binomcxplemdvbinom  38552  binomcxplemcvg  38553  binomcxplemnotnn0  38555  rfcnpre1  39178  rfcnpre2  39190  rfcnpre3  39192  rfcnpre4  39193  elpreimad  39454  limsupresxr  39998  liminfresxr  39999  icccncfext  40100  sge0fodjrnlem  40633  smfsuplem1  41017