Theorem elpreima 6828

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 5949	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3963	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6455	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2898	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	syl5ib 246	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6453	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6822	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 582	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 415	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 515	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6823	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6457	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 231	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 456	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 214	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  ^◡ccnv 5554  dom cdm 5555   “ cima 5558  Fun wfun 6349   Fn wfn 6350  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-fv 6363

This theorem is referenced by:  elpreimad  6829  fniniseg  6830  fncnvima2  6831  unpreima  6833  respreima  6836  fnse  7827  brwitnlem  8132  unxpwdom2  9052  smobeth  10008  fpwwe2lem6  10057  fpwwe2lem9  10060  hashkf  13693  isercolllem2  15022  isercolllem3  15023  isercoll  15024  fsumss  15082  fprodss  15302  tanval  15481  1arith  16263  0ram  16356  ghmpreima  18380  ghmnsgpreima  18383  torsubg  18974  kerf1ghm  19497  kerf1hrmOLD  19498  lmhmpreima  19820  mpfind  20320  znunithash  20711  cncnpi  21886  cncnp  21888  cnpdis  21901  cnt0  21954  cnhaus  21962  2ndcomap  22066  1stccnp  22070  ptpjpre1  22179  tx1cn  22217  tx2cn  22218  txcnmpt  22232  txdis1cn  22243  hauseqlcld  22254  xkoptsub  22262  xkococn  22268  kqsat  22339  kqcldsat  22341  kqreglem1  22349  kqreglem2  22350  reghmph  22401  ordthmeolem  22409  tmdcn2  22697  clssubg  22717  tgphaus  22725  qustgplem  22729  ucncn  22894  xmeterval  23042  imasf1obl  23098  blval2  23172  metuel2  23175  isnghm  23332  cnbl0  23382  cnblcld  23383  cnheiborlem  23558  nmhmcn  23724  ismbl  24127  mbfeqalem1  24242  mbfmulc2lem  24248  mbfmax  24250  mbfposr  24253  mbfimaopnlem  24256  mbfaddlem  24261  mbfsup  24265  i1f1lem  24290  i1fpos  24307  mbfi1fseqlem4  24319  itg2monolem1  24351  itg2gt0  24361  itg2cnlem1  24362  itg2cnlem2  24363  plyeq0lem  24800  dgrlem  24819  dgrub  24824  dgrlb  24826  pserulm  25010  psercnlem2  25012  psercnlem1  25013  psercn  25014  abelth  25029  eff1olem  25132  ellogrn  25143  dvloglem  25231  logf1o2  25233  efopnlem1  25239  efopnlem2  25240  logtayl  25243  cxpcn3lem  25328  cxpcn3  25329  resqrtcn  25330  asinneg  25464  areambl  25536  sqff1o  25759  ubthlem1  28647  unipreima  30391  1stpreima  30442  2ndpreima  30443  suppss3  30460  hashgt1  30530  tocyc01  30760  cyc3evpm  30792  kerunit  30896  smatrcl  31061  cnre2csqlem  31153  elzrhunit  31220  qqhval2lem  31222  qqhf  31227  1stmbfm  31518  2ndmbfm  31519  mbfmcnt  31526  eulerpartlemsv2  31616  eulerpartlemv  31622  eulerpartlemf  31628  eulerpartlemgvv  31634  eulerpartlemgh  31636  eulerpartlemgs2  31638  sseqmw  31649  sseqf  31650  sseqp1  31653  fiblem  31656  fibp1  31659  cvmseu  32523  cvmliftmolem1  32528  cvmliftmolem2  32529  cvmliftlem15  32545  cvmlift2lem10  32559  cvmlift3lem8  32573  elmthm  32823  mthmblem  32827  mclsppslem  32830  mclspps  32831  cnambfre  34955  dvtan  34957  ftc1anclem3  34984  ftc1anclem5  34986  areacirc  35002  sstotbnd2  35067  keridl  35325  ellkr  36240  pw2f1ocnv  39654  binomcxplemdvbinom  40705  binomcxplemcvg  40706  binomcxplemnotnn0  40708  rfcnpre1  41296  rfcnpre2  41308  rfcnpre3  41310  rfcnpre4  41311  limsupresxr  42067  liminfresxr  42068  icccncfext  42190  sge0fodjrnlem  42718  smfsuplem1  43105