Theorem elpreima 7033

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 6056	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3945	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6624	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2815	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6621	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7027	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7028	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6627	. . . 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 2109  ^◡ccnv 5640  dom cdm 5641   “ cima 5644  Fun wfun 6508   Fn wfn 6509  ‘cfv 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-fv 6522

This theorem is referenced by:  elpreimad  7034  fniniseg  7035  fncnvima2  7036  unpreima  7038  respreima  7041  fnse  8115  brwitnlem  8474  unxpwdom2  9548  smobeth  10546  fpwwe2lem5  10595  hashkf  14304  isercolllem2  15639  isercolllem3  15640  isercoll  15641  fsumss  15698  fprodss  15921  tanval  16103  1arith  16905  0ram  16998  ghmpreima  19177  ghmnsgpreima  19180  kerf1ghm  19186  torsubg  19791  lmhmpreima  20962  rhmpreimaidl  21194  znunithash  21481  mpfind  22021  cncnpi  23172  cncnp  23174  cnpdis  23187  cnt0  23240  cnhaus  23248  2ndcomap  23352  1stccnp  23356  ptpjpre1  23465  tx1cn  23503  tx2cn  23504  txcnmpt  23518  txdis1cn  23529  hauseqlcld  23540  xkoptsub  23548  xkococn  23554  kqsat  23625  kqcldsat  23627  kqreglem1  23635  kqreglem2  23636  reghmph  23687  ordthmeolem  23695  tmdcn2  23983  clssubg  24003  tgphaus  24011  qustgplem  24015  ucncn  24179  xmeterval  24327  imasf1obl  24383  blval2  24457  metuel2  24460  isnghm  24618  cnbl0  24668  cnblcld  24669  cnheiborlem  24860  nmhmcn  25027  ismbl  25434  mbfeqalem1  25549  mbfmulc2lem  25555  mbfmax  25557  mbfposr  25560  mbfimaopnlem  25563  mbfaddlem  25568  mbfsup  25572  i1f1lem  25597  i1fpos  25614  mbfi1fseqlem4  25626  itg2monolem1  25658  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  plyeq0lem  26122  dgrlem  26141  dgrub  26146  dgrlb  26148  pserulm  26338  psercnlem2  26341  psercnlem1  26342  psercn  26343  abelth  26358  eff1olem  26464  ellogrn  26475  dvloglem  26564  logf1o2  26566  efopnlem1  26572  efopnlem2  26573  logtayl  26576  cxpcn3lem  26664  cxpcn3  26665  resqrtcn  26666  asinneg  26803  areambl  26875  sqff1o  27099  ubthlem1  30806  unipreima  32574  suppiniseg  32616  1stpreima  32637  2ndpreima  32638  suppss3  32654  hashgt1  32740  pwrssmgc  32933  tocyc01  33082  cyc3evpm  33114  elrgspnsubrunlem2  33206  kerunit  33304  elrspunidl  33406  rhmpreimaprmidl  33429  ply1degltel  33567  ply1degleel  33568  ply1degltdimlem  33625  irngnminplynz  33709  smatrcl  33793  rhmpreimacnlem  33881  cnre2csqlem  33907  elzrhunit  33974  qqhval2lem  33978  qqhf  33983  1stmbfm  34258  2ndmbfm  34259  mbfmcnt  34266  eulerpartlemsv2  34356  eulerpartlemv  34362  eulerpartlemf  34368  eulerpartlemgvv  34374  eulerpartlemgh  34376  eulerpartlemgs2  34378  sseqmw  34389  sseqf  34390  sseqp1  34393  fiblem  34396  fibp1  34399  cvmseu  35270  cvmliftmolem1  35275  cvmliftmolem2  35276  cvmliftlem15  35292  cvmlift2lem10  35306  cvmlift3lem8  35320  elmthm  35570  mthmblem  35574  mclsppslem  35577  mclspps  35578  cnambfre  37669  dvtan  37671  ftc1anclem3  37696  ftc1anclem5  37698  areacirc  37714  sstotbnd2  37775  keridl  38033  ellkr  39089  pw2f1ocnv  43033  binomcxplemdvbinom  44349  binomcxplemcvg  44350  binomcxplemnotnn0  44352  permaxpow  45006  rfcnpre1  45020  rfcnpre2  45032  rfcnpre3  45034  rfcnpre4  45035  limsupresxr  45771  liminfresxr  45772  icccncfext  45892  sge0fodjrnlem  46421  smfsuplem1  46816