Theorem elpreima 6996

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 6037	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3933	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6589	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2814	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6586	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6990	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6991	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6592	. . . 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 2109  ^◡ccnv 5622  dom cdm 5623   “ cima 5626  Fun wfun 6480   Fn wfn 6481  ‘cfv 6486

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-fv 6494

This theorem is referenced by:  elpreimad  6997  fniniseg  6998  fncnvima2  6999  unpreima  7001  respreima  7004  fnse  8073  brwitnlem  8432  unxpwdom2  9499  smobeth  10499  fpwwe2lem5  10548  hashkf  14257  isercolllem2  15591  isercolllem3  15592  isercoll  15593  fsumss  15650  fprodss  15873  tanval  16055  1arith  16857  0ram  16950  ghmpreima  19135  ghmnsgpreima  19138  kerf1ghm  19144  torsubg  19751  lmhmpreima  20970  rhmpreimaidl  21202  znunithash  21489  mpfind  22030  cncnpi  23181  cncnp  23183  cnpdis  23196  cnt0  23249  cnhaus  23257  2ndcomap  23361  1stccnp  23365  ptpjpre1  23474  tx1cn  23512  tx2cn  23513  txcnmpt  23527  txdis1cn  23538  hauseqlcld  23549  xkoptsub  23557  xkococn  23563  kqsat  23634  kqcldsat  23636  kqreglem1  23644  kqreglem2  23645  reghmph  23696  ordthmeolem  23704  tmdcn2  23992  clssubg  24012  tgphaus  24020  qustgplem  24024  ucncn  24188  xmeterval  24336  imasf1obl  24392  blval2  24466  metuel2  24469  isnghm  24627  cnbl0  24677  cnblcld  24678  cnheiborlem  24869  nmhmcn  25036  ismbl  25443  mbfeqalem1  25558  mbfmulc2lem  25564  mbfmax  25566  mbfposr  25569  mbfimaopnlem  25572  mbfaddlem  25577  mbfsup  25581  i1f1lem  25606  i1fpos  25623  mbfi1fseqlem4  25635  itg2monolem1  25667  itg2gt0  25677  itg2cnlem1  25678  itg2cnlem2  25679  plyeq0lem  26131  dgrlem  26150  dgrub  26155  dgrlb  26157  pserulm  26347  psercnlem2  26350  psercnlem1  26351  psercn  26352  abelth  26367  eff1olem  26473  ellogrn  26484  dvloglem  26573  logf1o2  26575  efopnlem1  26581  efopnlem2  26582  logtayl  26585  cxpcn3lem  26673  cxpcn3  26674  resqrtcn  26675  asinneg  26812  areambl  26884  sqff1o  27108  ubthlem1  30832  unipreima  32600  suppiniseg  32642  1stpreima  32663  2ndpreima  32664  suppss3  32680  hashgt1  32766  pwrssmgc  32955  tocyc01  33073  cyc3evpm  33105  elrgspnsubrunlem2  33198  kerunit  33273  elrspunidl  33375  rhmpreimaprmidl  33398  ply1degltel  33536  ply1degleel  33537  ply1degltdimlem  33594  irngnminplynz  33678  smatrcl  33762  rhmpreimacnlem  33850  cnre2csqlem  33876  elzrhunit  33943  qqhval2lem  33947  qqhf  33952  1stmbfm  34227  2ndmbfm  34228  mbfmcnt  34235  eulerpartlemsv2  34325  eulerpartlemv  34331  eulerpartlemf  34337  eulerpartlemgvv  34343  eulerpartlemgh  34345  eulerpartlemgs2  34347  sseqmw  34358  sseqf  34359  sseqp1  34362  fiblem  34365  fibp1  34368  cvmseu  35248  cvmliftmolem1  35253  cvmliftmolem2  35254  cvmliftlem15  35270  cvmlift2lem10  35284  cvmlift3lem8  35298  elmthm  35548  mthmblem  35552  mclsppslem  35555  mclspps  35556  cnambfre  37647  dvtan  37649  ftc1anclem3  37674  ftc1anclem5  37676  areacirc  37692  sstotbnd2  37753  keridl  38011  ellkr  39067  pw2f1ocnv  43010  binomcxplemdvbinom  44326  binomcxplemcvg  44327  binomcxplemnotnn0  44329  permaxpow  44983  rfcnpre1  44997  rfcnpre2  45009  rfcnpre3  45011  rfcnpre4  45012  limsupresxr  45748  liminfresxr  45749  icccncfext  45869  sge0fodjrnlem  46398  smfsuplem1  46793