Theorem elpreima 7078

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 6100	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3979	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6671	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2827	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6668	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7072	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7073	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6674	. . . 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 2108  ^◡ccnv 5684  dom cdm 5685   “ cima 5688  Fun wfun 6555   Fn wfn 6556  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-fv 6569

This theorem is referenced by:  elpreimad  7079  fniniseg  7080  fncnvima2  7081  unpreima  7083  respreima  7086  fnse  8158  brwitnlem  8545  unxpwdom2  9628  smobeth  10626  fpwwe2lem5  10675  hashkf  14371  isercolllem2  15702  isercolllem3  15703  isercoll  15704  fsumss  15761  fprodss  15984  tanval  16164  1arith  16965  0ram  17058  ghmpreima  19256  ghmnsgpreima  19259  kerf1ghm  19265  torsubg  19872  lmhmpreima  21047  rhmpreimaidl  21287  znunithash  21583  mpfind  22131  cncnpi  23286  cncnp  23288  cnpdis  23301  cnt0  23354  cnhaus  23362  2ndcomap  23466  1stccnp  23470  ptpjpre1  23579  tx1cn  23617  tx2cn  23618  txcnmpt  23632  txdis1cn  23643  hauseqlcld  23654  xkoptsub  23662  xkococn  23668  kqsat  23739  kqcldsat  23741  kqreglem1  23749  kqreglem2  23750  reghmph  23801  ordthmeolem  23809  tmdcn2  24097  clssubg  24117  tgphaus  24125  qustgplem  24129  ucncn  24294  xmeterval  24442  imasf1obl  24501  blval2  24575  metuel2  24578  isnghm  24744  cnbl0  24794  cnblcld  24795  cnheiborlem  24986  nmhmcn  25153  ismbl  25561  mbfeqalem1  25676  mbfmulc2lem  25682  mbfmax  25684  mbfposr  25687  mbfimaopnlem  25690  mbfaddlem  25695  mbfsup  25699  i1f1lem  25724  i1fpos  25741  mbfi1fseqlem4  25753  itg2monolem1  25785  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  plyeq0lem  26249  dgrlem  26268  dgrub  26273  dgrlb  26275  pserulm  26465  psercnlem2  26468  psercnlem1  26469  psercn  26470  abelth  26485  eff1olem  26590  ellogrn  26601  dvloglem  26690  logf1o2  26692  efopnlem1  26698  efopnlem2  26699  logtayl  26702  cxpcn3lem  26790  cxpcn3  26791  resqrtcn  26792  asinneg  26929  areambl  27001  sqff1o  27225  ubthlem1  30889  unipreima  32653  suppiniseg  32695  1stpreima  32716  2ndpreima  32717  suppss3  32735  hashgt1  32812  pwrssmgc  32990  tocyc01  33138  cyc3evpm  33170  elrgspnsubrunlem2  33252  kerunit  33349  elrspunidl  33456  rhmpreimaprmidl  33479  ply1degltel  33615  ply1degleel  33616  ply1degltdimlem  33673  irngnminplynz  33755  smatrcl  33795  rhmpreimacnlem  33883  cnre2csqlem  33909  elzrhunit  33978  qqhval2lem  33982  qqhf  33987  1stmbfm  34262  2ndmbfm  34263  mbfmcnt  34270  eulerpartlemsv2  34360  eulerpartlemv  34366  eulerpartlemf  34372  eulerpartlemgvv  34378  eulerpartlemgh  34380  eulerpartlemgs2  34382  sseqmw  34393  sseqf  34394  sseqp1  34397  fiblem  34400  fibp1  34403  cvmseu  35281  cvmliftmolem1  35286  cvmliftmolem2  35287  cvmliftlem15  35303  cvmlift2lem10  35317  cvmlift3lem8  35331  elmthm  35581  mthmblem  35585  mclsppslem  35588  mclspps  35589  cnambfre  37675  dvtan  37677  ftc1anclem3  37702  ftc1anclem5  37704  areacirc  37720  sstotbnd2  37781  keridl  38039  ellkr  39090  pw2f1ocnv  43049  binomcxplemdvbinom  44372  binomcxplemcvg  44373  binomcxplemnotnn0  44375  rfcnpre1  45024  rfcnpre2  45036  rfcnpre3  45038  rfcnpre4  45039  limsupresxr  45781  liminfresxr  45782  icccncfext  45902  sge0fodjrnlem  46431  smfsuplem1  46826