Theorem elpreima 7055

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 6086	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3934	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6640	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2849	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 247	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6637	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7049	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 591	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 417	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 521	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7050	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6643	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 232	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 458	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 215	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  ^◡ccnv 5662  dom cdm 5663   “ cima 5666  Fun wfun 6532   Fn wfn 6533  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546

This theorem is referenced by:  elpreimad  7056  fniniseg  7057  fncnvima2  7058  unpreima  7060  respreima  7063  fnse  8130  brwitnlem  8493  unxpwdom2  9551  smobeth  10572  fpwwe2lem5  10621  hashkf  14370  isercolllem2  15719  isercolllem3  15720  isercoll  15721  fsumss  15778  fprodss  16004  tanval  16185  1arith  16988  0ram  17081  ghmpreima  19309  ghmnsgpreima  19312  kerf1ghm  19318  torsubg  19925  lmhmpreima  21150  rhmpreimaidl  21397  rhmpreimaprmidl  21460  znunithash  21695  mpfind  22247  cncnpi  23416  cncnp  23418  cnpdis  23431  cnt0  23484  cnhaus  23492  2ndcomap  23596  1stccnp  23600  ptpjpre1  23709  tx1cn  23747  tx2cn  23748  txcnmpt  23762  txdis1cn  23773  hauseqlcld  23784  xkoptsub  23792  xkococn  23798  kqsat  23869  kqcldsat  23871  kqreglem1  23879  kqreglem2  23880  reghmph  23931  ordthmeolem  23939  tmdcn2  24227  clssubg  24247  tgphaus  24255  qustgplem  24259  ucncn  24422  xmeterval  24570  imasf1obl  24626  blval2  24700  metuel2  24703  isnghm  24861  cnbl0  24911  cnblcld  24912  cnheiborlem  25094  nmhmcn  25260  ismbl  25666  mbfeqalem1  25781  mbfmulc2lem  25787  mbfmax  25789  mbfposr  25792  mbfimaopnlem  25795  mbfaddlem  25800  mbfsup  25804  i1f1lem  25829  i1fpos  25846  mbfi1fseqlem4  25858  itg2monolem1  25890  itg2gt0  25900  itg2cnlem1  25901  itg2cnlem2  25902  plyeq0lem  26348  dgrlem  26367  dgrub  26372  dgrlb  26374  pserulm  26563  psercnlem2  26565  psercnlem1  26566  psercn  26567  abelth  26582  eff1olem  26691  ellogrn  26702  dvloglem  26791  logf1o2  26793  efopnlem1  26799  efopnlem2  26800  logtayl  26803  cxpcn3lem  26890  cxpcn3  26891  resqrtcn  26892  asinneg  27029  areambl  27101  sqff1o  27324  ubthlem1  31200  unipreima  32966  suppiniseg  33009  1stpreima  33030  2ndpreima  33031  suppss3  33046  hashgt1  33131  pwrssmgc  33298  tocyc01  33416  cyc3evpm  33448  elrgspnsubrunlem2  33546  kerunit  33623  elrspunidl  33714  ply1degltel  33862  ply1degleel  33863  ply1degltdimlem  33990  irngnminplynz  34080  smatrcl  34164  rhmpreimacnlem  34252  cnre2csqlem  34278  elzrhunit  34345  qqhval2lem  34349  qqhf  34354  1stmbfm  34628  2ndmbfm  34629  mbfmcnt  34636  eulerpartlemsv2  34726  eulerpartlemv  34732  eulerpartlemf  34738  eulerpartlemgvv  34744  eulerpartlemgh  34746  eulerpartlemgs2  34748  sseqmw  34759  sseqf  34760  sseqp1  34763  fiblem  34766  fibp1  34769  cvmseu  35746  cvmliftmolem1  35751  cvmliftmolem2  35752  cvmliftlem15  35768  cvmlift2lem10  35782  cvmlift3lem8  35796  elmthm  36046  mthmblem  36050  mclsppslem  36053  mclspps  36054  cnambfre  38297  dvtan  38299  ftc1anclem3  38324  ftc1anclem5  38326  areacirc  38342  sstotbnd2  38403  keridl  38661  ellkr  39841  pw2f1ocnv  43744  binomcxplemdvbinom  45043  binomcxplemcvg  45044  binomcxplemnotnn0  45046  permaxpow  45698  rfcnpre1  45719  rfcnpre2  45731  rfcnpre3  45733  rfcnpre4  45734  limsupresxr  46460  liminfresxr  46461  icccncfext  46581  sge0fodjrnlem  47110  smfsuplem1  47505