Theorem elpreima 7076

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 6096	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3987	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6667	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2815	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 243	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6664	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7070	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 578	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 411	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 511	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7071	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6670	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 228	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 452	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 211	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∈ wcel 2100  ^◡ccnv 5685  dom cdm 5686   “ cima 5689  Fun wfun 6552   Fn wfn 6553  ‘cfv 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pr 5437

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-ne 2934  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-id 5584  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-iota 6510  df-fun 6560  df-fn 6561  df-fv 6566

This theorem is referenced by:  elpreimad  7077  fniniseg  7078  fncnvima2  7079  unpreima  7081  respreima  7084  fnse  8155  brwitnlem  8545  unxpwdom2  9638  smobeth  10636  fpwwe2lem5  10685  hashkf  14361  isercolllem2  15691  isercolllem3  15692  isercoll  15693  fsumss  15750  fprodss  15971  tanval  16151  1arith  16950  0ram  17043  ghmpreima  19254  ghmnsgpreima  19257  kerf1ghm  19263  torsubg  19874  lmhmpreima  21048  rhmpreimaidl  21288  znunithash  21584  mpfind  22144  cncnpi  23296  cncnp  23298  cnpdis  23311  cnt0  23364  cnhaus  23372  2ndcomap  23476  1stccnp  23480  ptpjpre1  23589  tx1cn  23627  tx2cn  23628  txcnmpt  23642  txdis1cn  23653  hauseqlcld  23664  xkoptsub  23672  xkococn  23678  kqsat  23749  kqcldsat  23751  kqreglem1  23759  kqreglem2  23760  reghmph  23811  ordthmeolem  23819  tmdcn2  24107  clssubg  24127  tgphaus  24135  qustgplem  24139  ucncn  24304  xmeterval  24452  imasf1obl  24511  blval2  24585  metuel2  24588  isnghm  24754  cnbl0  24804  cnblcld  24805  cnheiborlem  24994  nmhmcn  25161  ismbl  25569  mbfeqalem1  25684  mbfmulc2lem  25690  mbfmax  25692  mbfposr  25695  mbfimaopnlem  25698  mbfaddlem  25703  mbfsup  25707  i1f1lem  25732  i1fpos  25750  mbfi1fseqlem4  25762  itg2monolem1  25794  itg2gt0  25804  itg2cnlem1  25805  itg2cnlem2  25806  plyeq0lem  26260  dgrlem  26279  dgrub  26284  dgrlb  26286  pserulm  26474  psercnlem2  26477  psercnlem1  26478  psercn  26479  abelth  26494  eff1olem  26598  ellogrn  26609  dvloglem  26698  logf1o2  26700  efopnlem1  26706  efopnlem2  26707  logtayl  26710  cxpcn3lem  26798  cxpcn3  26799  resqrtcn  26800  asinneg  26937  areambl  27009  sqff1o  27233  ubthlem1  30826  unipreima  32587  suppiniseg  32623  1stpreima  32643  2ndpreima  32644  suppss3  32663  hashgt1  32740  pwrssmgc  32898  tocyc01  33025  cyc3evpm  33057  kerunit  33227  elrspunidl  33334  rhmpreimaprmidl  33357  ply1degltel  33493  ply1degleel  33494  ply1degltdimlem  33548  irngnminplynz  33612  smatrcl  33649  rhmpreimacnlem  33737  cnre2csqlem  33763  elzrhunit  33832  qqhval2lem  33834  qqhf  33839  1stmbfm  34132  2ndmbfm  34133  mbfmcnt  34140  eulerpartlemsv2  34230  eulerpartlemv  34236  eulerpartlemf  34242  eulerpartlemgvv  34248  eulerpartlemgh  34250  eulerpartlemgs2  34252  sseqmw  34263  sseqf  34264  sseqp1  34267  fiblem  34270  fibp1  34273  cvmseu  35151  cvmliftmolem1  35156  cvmliftmolem2  35157  cvmliftlem15  35173  cvmlift2lem10  35187  cvmlift3lem8  35201  elmthm  35451  mthmblem  35455  mclsppslem  35458  mclspps  35459  cnambfre  37416  dvtan  37418  ftc1anclem3  37443  ftc1anclem5  37445  areacirc  37461  sstotbnd2  37522  keridl  37780  ellkr  38834  pw2f1ocnv  42766  binomcxplemdvbinom  44098  binomcxplemcvg  44099  binomcxplemnotnn0  44101  rfcnpre1  44689  rfcnpre2  44701  rfcnpre3  44703  rfcnpre4  44704  limsupresxr  45457  liminfresxr  45458  icccncfext  45578  sge0fodjrnlem  46107  smfsuplem1  46502