Theorem elpreima 7013

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 6038	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3943	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6610	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2818	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 243	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6607	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7007	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 413	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 513	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7008	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6613	. . . 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 2106  ^◡ccnv 5637  dom cdm 5638   “ cima 5641  Fun wfun 6495   Fn wfn 6496  ‘cfv 6501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-fv 6509

This theorem is referenced by:  elpreimad  7014  fniniseg  7015  fncnvima2  7016  unpreima  7018  respreima  7021  fnse  8070  brwitnlem  8458  unxpwdom2  9533  smobeth  10531  fpwwe2lem5  10580  hashkf  14242  isercolllem2  15562  isercolllem3  15563  isercoll  15564  fsumss  15621  fprodss  15842  tanval  16021  1arith  16810  0ram  16903  ghmpreima  19044  ghmnsgpreima  19047  torsubg  19646  kerf1ghm  20193  lmhmpreima  20566  znunithash  21008  mpfind  21554  cncnpi  22666  cncnp  22668  cnpdis  22681  cnt0  22734  cnhaus  22742  2ndcomap  22846  1stccnp  22850  ptpjpre1  22959  tx1cn  22997  tx2cn  22998  txcnmpt  23012  txdis1cn  23023  hauseqlcld  23034  xkoptsub  23042  xkococn  23048  kqsat  23119  kqcldsat  23121  kqreglem1  23129  kqreglem2  23130  reghmph  23181  ordthmeolem  23189  tmdcn2  23477  clssubg  23497  tgphaus  23505  qustgplem  23509  ucncn  23674  xmeterval  23822  imasf1obl  23881  blval2  23955  metuel2  23958  isnghm  24124  cnbl0  24174  cnblcld  24175  cnheiborlem  24354  nmhmcn  24520  ismbl  24927  mbfeqalem1  25042  mbfmulc2lem  25048  mbfmax  25050  mbfposr  25053  mbfimaopnlem  25056  mbfaddlem  25061  mbfsup  25065  i1f1lem  25090  i1fpos  25108  mbfi1fseqlem4  25120  itg2monolem1  25152  itg2gt0  25162  itg2cnlem1  25163  itg2cnlem2  25164  plyeq0lem  25608  dgrlem  25627  dgrub  25632  dgrlb  25634  pserulm  25818  psercnlem2  25820  psercnlem1  25821  psercn  25822  abelth  25837  eff1olem  25941  ellogrn  25952  dvloglem  26040  logf1o2  26042  efopnlem1  26048  efopnlem2  26049  logtayl  26052  cxpcn3lem  26137  cxpcn3  26138  resqrtcn  26139  asinneg  26273  areambl  26345  sqff1o  26568  ubthlem1  29875  unipreima  31627  suppiniseg  31668  1stpreima  31688  2ndpreima  31689  suppss3  31709  hashgt1  31780  pwrssmgc  31930  tocyc01  32037  cyc3evpm  32069  kerunit  32185  rhmpreimaidl  32275  elrspunidl  32279  rhmpreimaprmidl  32300  ply1degltel  32365  ply1degltdimlem  32404  smatrcl  32466  rhmpreimacnlem  32554  cnre2csqlem  32580  elzrhunit  32649  qqhval2lem  32651  qqhf  32656  1stmbfm  32949  2ndmbfm  32950  mbfmcnt  32957  eulerpartlemsv2  33047  eulerpartlemv  33053  eulerpartlemf  33059  eulerpartlemgvv  33065  eulerpartlemgh  33067  eulerpartlemgs2  33069  sseqmw  33080  sseqf  33081  sseqp1  33084  fiblem  33087  fibp1  33090  cvmseu  33957  cvmliftmolem1  33962  cvmliftmolem2  33963  cvmliftlem15  33979  cvmlift2lem10  33993  cvmlift3lem8  34007  elmthm  34257  mthmblem  34261  mclsppslem  34264  mclspps  34265  cnambfre  36199  dvtan  36201  ftc1anclem3  36226  ftc1anclem5  36228  areacirc  36244  sstotbnd2  36306  keridl  36564  ellkr  37624  pw2f1ocnv  41419  binomcxplemdvbinom  42755  binomcxplemcvg  42756  binomcxplemnotnn0  42758  rfcnpre1  43346  rfcnpre2  43358  rfcnpre3  43360  rfcnpre4  43361  limsupresxr  44127  liminfresxr  44128  icccncfext  44248  sge0fodjrnlem  44777  smfsuplem1  45172