Theorem elpreima 7059

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 6080	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3978	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6652	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2819	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 243	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6649	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7053	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 413	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 513	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7054	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6655	. . . 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 5675  dom cdm 5676   “ cima 5679  Fun wfun 6537   Fn wfn 6538  ‘cfv 6543

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 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-fv 6551

This theorem is referenced by:  elpreimad  7060  fniniseg  7061  fncnvima2  7062  unpreima  7064  respreima  7067  fnse  8121  brwitnlem  8509  unxpwdom2  9585  smobeth  10583  fpwwe2lem5  10632  hashkf  14294  isercolllem2  15614  isercolllem3  15615  isercoll  15616  fsumss  15673  fprodss  15894  tanval  16073  1arith  16862  0ram  16955  ghmpreima  19116  ghmnsgpreima  19119  torsubg  19724  kerf1ghm  20286  lmhmpreima  20664  znunithash  21126  mpfind  21676  cncnpi  22789  cncnp  22791  cnpdis  22804  cnt0  22857  cnhaus  22865  2ndcomap  22969  1stccnp  22973  ptpjpre1  23082  tx1cn  23120  tx2cn  23121  txcnmpt  23135  txdis1cn  23146  hauseqlcld  23157  xkoptsub  23165  xkococn  23171  kqsat  23242  kqcldsat  23244  kqreglem1  23252  kqreglem2  23253  reghmph  23304  ordthmeolem  23312  tmdcn2  23600  clssubg  23620  tgphaus  23628  qustgplem  23632  ucncn  23797  xmeterval  23945  imasf1obl  24004  blval2  24078  metuel2  24081  isnghm  24247  cnbl0  24297  cnblcld  24298  cnheiborlem  24477  nmhmcn  24643  ismbl  25050  mbfeqalem1  25165  mbfmulc2lem  25171  mbfmax  25173  mbfposr  25176  mbfimaopnlem  25179  mbfaddlem  25184  mbfsup  25188  i1f1lem  25213  i1fpos  25231  mbfi1fseqlem4  25243  itg2monolem1  25275  itg2gt0  25285  itg2cnlem1  25286  itg2cnlem2  25287  plyeq0lem  25731  dgrlem  25750  dgrub  25755  dgrlb  25757  pserulm  25941  psercnlem2  25943  psercnlem1  25944  psercn  25945  abelth  25960  eff1olem  26064  ellogrn  26075  dvloglem  26163  logf1o2  26165  efopnlem1  26171  efopnlem2  26172  logtayl  26175  cxpcn3lem  26262  cxpcn3  26263  resqrtcn  26264  asinneg  26398  areambl  26470  sqff1o  26693  ubthlem1  30161  unipreima  31907  suppiniseg  31946  1stpreima  31966  2ndpreima  31967  suppss3  31987  hashgt1  32058  pwrssmgc  32208  tocyc01  32318  cyc3evpm  32350  kerunit  32478  rhmpreimaidl  32582  elrspunidl  32591  rhmpreimaprmidl  32615  ply1degltel  32711  ply1degleel  32712  ply1degltdimlem  32766  irngnminplynz  32831  smatrcl  32845  rhmpreimacnlem  32933  cnre2csqlem  32959  elzrhunit  33028  qqhval2lem  33030  qqhf  33035  1stmbfm  33328  2ndmbfm  33329  mbfmcnt  33336  eulerpartlemsv2  33426  eulerpartlemv  33432  eulerpartlemf  33438  eulerpartlemgvv  33444  eulerpartlemgh  33446  eulerpartlemgs2  33448  sseqmw  33459  sseqf  33460  sseqp1  33463  fiblem  33466  fibp1  33469  cvmseu  34336  cvmliftmolem1  34341  cvmliftmolem2  34342  cvmliftlem15  34358  cvmlift2lem10  34372  cvmlift3lem8  34386  elmthm  34636  mthmblem  34640  mclsppslem  34643  mclspps  34644  cnambfre  36622  dvtan  36624  ftc1anclem3  36649  ftc1anclem5  36651  areacirc  36667  sstotbnd2  36728  keridl  36986  ellkr  38045  pw2f1ocnv  41858  binomcxplemdvbinom  43194  binomcxplemcvg  43195  binomcxplemnotnn0  43197  rfcnpre1  43785  rfcnpre2  43797  rfcnpre3  43799  rfcnpre4  43800  limsupresxr  44561  liminfresxr  44562  icccncfext  44682  sge0fodjrnlem  45211  smfsuplem1  45606