Theorem elpreima 6245

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 5404	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3564	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 5904	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2673	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	syl5ib 233	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 5902	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6239	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 487	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 449	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 554	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6240	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 5905	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 218	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 627	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 201	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  ^◡ccnv 5037  dom cdm 5038   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812

This theorem is referenced by:  fniniseg  6246  fncnvima2  6247  unpreima  6249  respreima  6252  fnse  7181  brwitnlem  7474  unxpwdom2  8376  smobeth  9287  fpwwe2lem6  9336  fpwwe2lem9  9339  hashkf  12981  isercolllem2  14244  isercolllem3  14245  isercoll  14246  fsumss  14303  fprodss  14517  tanval  14697  1arith  15469  0ram  15562  ghmpreima  17505  ghmnsgpreima  17508  torsubg  18080  kerf1hrm  18566  lmhmpreima  18869  evlslem3  19335  mpfind  19357  znunithash  19732  cncnpi  20892  cncnp  20894  cnpdis  20907  cnt0  20960  cnhaus  20968  2ndcomap  21071  1stccnp  21075  ptpjpre1  21184  tx1cn  21222  tx2cn  21223  txcnmpt  21237  txdis1cn  21248  hauseqlcld  21259  xkoptsub  21267  xkococn  21273  kqsat  21344  kqcldsat  21346  kqreglem1  21354  kqreglem2  21355  reghmph  21406  ordthmeolem  21414  tmdcn2  21703  clssubg  21722  tgphaus  21730  qustgplem  21734  ucncn  21899  xmeterval  22047  imasf1obl  22103  blval2  22177  metuel2  22180  isnghm  22337  cnbl0  22387  cnblcld  22388  cnheiborlem  22561  nmhmcn  22728  ismbl  23101  mbfeqalem  23215  mbfmulc2lem  23220  mbfmax  23222  mbfposr  23225  mbfimaopnlem  23228  mbfaddlem  23233  mbfsup  23237  i1f1lem  23262  i1fpos  23279  mbfi1fseqlem4  23291  itg2monolem1  23323  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  plyeq0lem  23770  dgrlem  23789  dgrub  23794  dgrlb  23796  pserulm  23980  psercnlem2  23982  psercnlem1  23983  psercn  23984  abelth  23999  eff1olem  24098  ellogrn  24110  dvloglem  24194  logf1o2  24196  efopnlem1  24202  efopnlem2  24203  logtayl  24206  cxpcn3lem  24288  cxpcn3  24289  resqrtcn  24290  asinneg  24413  areambl  24485  sqff1o  24708  ubthlem1  27110  unipreima  28826  1stpreima  28867  2ndpreima  28868  suppss3  28890  kerunit  29154  smatrcl  29190  cnre2csqlem  29284  elzrhunit  29351  qqhval2lem  29353  qqhf  29358  1stmbfm  29649  2ndmbfm  29650  mbfmcnt  29657  eulerpartlemsv2  29747  eulerpartlemv  29753  eulerpartlemf  29759  eulerpartlemgvv  29765  eulerpartlemgh  29767  eulerpartlemgs2  29769  sseqmw  29780  sseqf  29781  sseqp1  29784  fiblem  29787  fibp1  29790  cvmseu  30512  cvmliftmolem1  30517  cvmliftmolem2  30518  cvmliftlem15  30534  cvmlift2lem10  30548  cvmlift3lem8  30562  elmthm  30727  mthmblem  30731  mclsppslem  30734  mclspps  30735  cnambfre  32628  dvtan  32630  ftc1anclem3  32657  ftc1anclem5  32659  areacirc  32675  sstotbnd2  32743  keridl  33001  ellkr  33394  pw2f1ocnv  36622  binomcxplemdvbinom  37574  binomcxplemcvg  37575  binomcxplemnotnn0  37577  rfcnpre1  38201  rfcnpre2  38213  rfcnpre3  38215  rfcnpre4  38216  icccncfext  38773  sge0fodjrnlem  39309