Theorem elpreima 7035

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 6068	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3932	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6620	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2847	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 246	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6617	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7029	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 589	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 416	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 520	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7030	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6623	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 231	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 457	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 214	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2141  ^◡ccnv 5644  dom cdm 5645   “ cima 5648  Fun wfun 6511   Fn wfn 6512  ‘cfv 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-fv 6525

This theorem is referenced by:  elpreimad  7036  fniniseg  7037  fncnvima2  7038  unpreima  7040  respreima  7043  fnse  8108  brwitnlem  8471  unxpwdom2  9533  smobeth  10541  fpwwe2lem5  10590  hashkf  14342  isercolllem2  15676  isercolllem3  15677  isercoll  15678  fsumss  15735  fprodss  15961  tanval  16143  1arith  16946  0ram  17039  ghmpreima  19261  ghmnsgpreima  19264  kerf1ghm  19270  torsubg  19877  lmhmpreima  21095  rhmpreimaidl  21327  znunithash  21596  mpfind  22148  cncnpi  23318  cncnp  23320  cnpdis  23333  cnt0  23386  cnhaus  23394  2ndcomap  23498  1stccnp  23502  ptpjpre1  23611  tx1cn  23649  tx2cn  23650  txcnmpt  23664  txdis1cn  23675  hauseqlcld  23686  xkoptsub  23694  xkococn  23700  kqsat  23771  kqcldsat  23773  kqreglem1  23781  kqreglem2  23782  reghmph  23833  ordthmeolem  23841  tmdcn2  24129  clssubg  24149  tgphaus  24157  qustgplem  24161  ucncn  24324  xmeterval  24472  imasf1obl  24528  blval2  24602  metuel2  24605  isnghm  24763  cnbl0  24813  cnblcld  24814  cnheiborlem  24996  nmhmcn  25162  ismbl  25568  mbfeqalem1  25683  mbfmulc2lem  25689  mbfmax  25691  mbfposr  25694  mbfimaopnlem  25697  mbfaddlem  25702  mbfsup  25706  i1f1lem  25731  i1fpos  25748  mbfi1fseqlem4  25760  itg2monolem1  25792  itg2gt0  25802  itg2cnlem1  25803  itg2cnlem2  25804  plyeq0lem  26250  dgrlem  26269  dgrub  26274  dgrlb  26276  pserulm  26462  psercnlem2  26464  psercnlem1  26465  psercn  26466  abelth  26481  eff1olem  26590  ellogrn  26601  dvloglem  26690  logf1o2  26692  efopnlem1  26698  efopnlem2  26699  logtayl  26702  cxpcn3lem  26789  cxpcn3  26790  resqrtcn  26791  asinneg  26928  areambl  27000  sqff1o  27223  ubthlem1  31019  unipreima  32795  suppiniseg  32838  1stpreima  32859  2ndpreima  32860  suppss3  32875  hashgt1  32960  pwrssmgc  33139  tocyc01  33259  cyc3evpm  33291  elrgspnsubrunlem2  33390  kerunit  33472  elrspunidl  33575  rhmpreimaprmidl  33599  ply1degltel  33751  ply1degleel  33752  ply1degltdimlem  33880  irngnminplynz  33970  smatrcl  34054  rhmpreimacnlem  34142  cnre2csqlem  34168  elzrhunit  34235  qqhval2lem  34239  qqhf  34244  1stmbfm  34518  2ndmbfm  34519  mbfmcnt  34526  eulerpartlemsv2  34616  eulerpartlemv  34622  eulerpartlemf  34628  eulerpartlemgvv  34634  eulerpartlemgh  34636  eulerpartlemgs2  34638  sseqmw  34649  sseqf  34650  sseqp1  34653  fiblem  34656  fibp1  34659  cvmseu  35590  cvmliftmolem1  35595  cvmliftmolem2  35596  cvmliftlem15  35612  cvmlift2lem10  35626  cvmlift3lem8  35640  elmthm  35890  mthmblem  35894  mclsppslem  35897  mclspps  35898  cnambfre  38131  dvtan  38133  ftc1anclem3  38158  ftc1anclem5  38160  areacirc  38176  sstotbnd2  38237  keridl  38495  ellkr  39677  pw2f1ocnv  43578  binomcxplemdvbinom  44893  binomcxplemcvg  44894  binomcxplemnotnn0  44896  permaxpow  45549  rfcnpre1  45563  rfcnpre2  45575  rfcnpre3  45577  rfcnpre4  45578  limsupresxr  46304  liminfresxr  46305  icccncfext  46425  sge0fodjrnlem  46954  smfsuplem1  47349