Theorem elpreima 7077

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 6101	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3990	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6671	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2824	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6668	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7071	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7072	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6674	. . . 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 2105  ^◡ccnv 5687  dom cdm 5688   “ cima 5691  Fun wfun 6556   Fn wfn 6557  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-fv 6570

This theorem is referenced by:  elpreimad  7078  fniniseg  7079  fncnvima2  7080  unpreima  7082  respreima  7085  fnse  8156  brwitnlem  8543  unxpwdom2  9625  smobeth  10623  fpwwe2lem5  10672  hashkf  14367  isercolllem2  15698  isercolllem3  15699  isercoll  15700  fsumss  15757  fprodss  15980  tanval  16160  1arith  16960  0ram  17053  ghmpreima  19268  ghmnsgpreima  19271  kerf1ghm  19277  torsubg  19886  lmhmpreima  21064  rhmpreimaidl  21304  znunithash  21600  mpfind  22148  cncnpi  23301  cncnp  23303  cnpdis  23316  cnt0  23369  cnhaus  23377  2ndcomap  23481  1stccnp  23485  ptpjpre1  23594  tx1cn  23632  tx2cn  23633  txcnmpt  23647  txdis1cn  23658  hauseqlcld  23669  xkoptsub  23677  xkococn  23683  kqsat  23754  kqcldsat  23756  kqreglem1  23764  kqreglem2  23765  reghmph  23816  ordthmeolem  23824  tmdcn2  24112  clssubg  24132  tgphaus  24140  qustgplem  24144  ucncn  24309  xmeterval  24457  imasf1obl  24516  blval2  24590  metuel2  24593  isnghm  24759  cnbl0  24809  cnblcld  24810  cnheiborlem  24999  nmhmcn  25166  ismbl  25574  mbfeqalem1  25689  mbfmulc2lem  25695  mbfmax  25697  mbfposr  25700  mbfimaopnlem  25703  mbfaddlem  25708  mbfsup  25712  i1f1lem  25737  i1fpos  25755  mbfi1fseqlem4  25767  itg2monolem1  25799  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  plyeq0lem  26263  dgrlem  26282  dgrub  26287  dgrlb  26289  pserulm  26479  psercnlem2  26482  psercnlem1  26483  psercn  26484  abelth  26499  eff1olem  26604  ellogrn  26615  dvloglem  26704  logf1o2  26706  efopnlem1  26712  efopnlem2  26713  logtayl  26716  cxpcn3lem  26804  cxpcn3  26805  resqrtcn  26806  asinneg  26943  areambl  27015  sqff1o  27239  ubthlem1  30898  unipreima  32659  suppiniseg  32700  1stpreima  32721  2ndpreima  32722  suppss3  32741  hashgt1  32817  pwrssmgc  32974  tocyc01  33120  cyc3evpm  33152  kerunit  33328  elrspunidl  33435  rhmpreimaprmidl  33458  ply1degltel  33594  ply1degleel  33595  ply1degltdimlem  33649  irngnminplynz  33719  smatrcl  33756  rhmpreimacnlem  33844  cnre2csqlem  33870  elzrhunit  33939  qqhval2lem  33943  qqhf  33948  1stmbfm  34241  2ndmbfm  34242  mbfmcnt  34249  eulerpartlemsv2  34339  eulerpartlemv  34345  eulerpartlemf  34351  eulerpartlemgvv  34357  eulerpartlemgh  34359  eulerpartlemgs2  34361  sseqmw  34372  sseqf  34373  sseqp1  34376  fiblem  34379  fibp1  34382  cvmseu  35260  cvmliftmolem1  35265  cvmliftmolem2  35266  cvmliftlem15  35282  cvmlift2lem10  35296  cvmlift3lem8  35310  elmthm  35560  mthmblem  35564  mclsppslem  35567  mclspps  35568  cnambfre  37654  dvtan  37656  ftc1anclem3  37681  ftc1anclem5  37683  areacirc  37699  sstotbnd2  37760  keridl  38018  ellkr  39070  pw2f1ocnv  43025  binomcxplemdvbinom  44348  binomcxplemcvg  44349  binomcxplemnotnn0  44351  rfcnpre1  44956  rfcnpre2  44968  rfcnpre3  44970  rfcnpre4  44971  limsupresxr  45721  liminfresxr  45722  icccncfext  45842  sge0fodjrnlem  46371  smfsuplem1  46766