MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fmpt Structured version   Visualization version   GIF version

Theorem fmpt 7054
Description: Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypothesis
Ref Expression
fmpt.1 𝐹 = (𝑥𝐴𝐶)
Assertion
Ref Expression
fmpt (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝐶(𝑥)   𝐹(𝑥)

Proof of Theorem fmpt
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 fmpt.1 . . . 4 𝐹 = (𝑥𝐴𝐶)
21fnmpt 6638 . . 3 (∀𝑥𝐴 𝐶𝐵𝐹 Fn 𝐴)
31rnmpt 5908 . . . 4 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶}
4 r19.29 3115 . . . . . . 7 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → ∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶))
5 eleq1 2825 . . . . . . . . 9 (𝑦 = 𝐶 → (𝑦𝐵𝐶𝐵))
65biimparc 480 . . . . . . . 8 ((𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
76rexlimivw 3146 . . . . . . 7 (∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
84, 7syl 17 . . . . . 6 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → 𝑦𝐵)
98ex 413 . . . . 5 (∀𝑥𝐴 𝐶𝐵 → (∃𝑥𝐴 𝑦 = 𝐶𝑦𝐵))
109abssdv 4023 . . . 4 (∀𝑥𝐴 𝐶𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶} ⊆ 𝐵)
113, 10eqsstrid 3990 . . 3 (∀𝑥𝐴 𝐶𝐵 → ran 𝐹𝐵)
12 df-f 6497 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
132, 11, 12sylanbrc 583 . 2 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
14 fimacnv 6687 . . . 4 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐴)
151mptpreima 6188 . . . 4 (𝐹𝐵) = {𝑥𝐴𝐶𝐵}
1614, 15eqtr3di 2791 . . 3 (𝐹:𝐴𝐵𝐴 = {𝑥𝐴𝐶𝐵})
17 rabid2 3434 . . 3 (𝐴 = {𝑥𝐴𝐶𝐵} ↔ ∀𝑥𝐴 𝐶𝐵)
1816, 17sylib 217 . 2 (𝐹:𝐴𝐵 → ∀𝑥𝐴 𝐶𝐵)
1913, 18impbii 208 1 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wcel 2106  {cab 2713  wral 3062  wrex 3071  {crab 3405  wss 3908  cmpt 5186  ccnv 5630  ran crn 5632  cima 5634   Fn wfn 6488  wf 6489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6495  df-fn 6496  df-f 6497
This theorem is referenced by:  f1ompt  7055  fmpti  7056  fvmptelcdm  7057  fmptd  7058  fmptdf  7061  rnmptss  7066  f1oresrab  7069  idref  7088  f1mpt  7204  f1stres  7941  f2ndres  7942  fmpox  7995  fmpoco  8023  onoviun  8285  onnseq  8286  mptelixpg  8869  dom2lem  8928  iinfi  9349  cantnfrescl  9608  acni2  9978  acnlem  9980  dfac4  10054  dfacacn  10073  fin23lem28  10272  axdc2lem  10380  axcclem  10389  ac6num  10411  uzf  12762  ccatalpha  14473  repsf  14653  rlim2  15370  rlimi  15387  o1fsum  15690  ackbijnn  15705  pcmptcl  16755  vdwlem11  16855  ismon2  17609  isepi2  17616  yonedalem3b  18160  smndex1gbas  18704  efgsf  19502  gsummhm2  19707  gsummptcl  19735  gsummptfif1o  19736  gsummptfzcl  19737  gsumcom2  19743  gsummptnn0fz  19754  issrngd  20305  ipcl  21022  subrgasclcl  21459  evl1sca  21684  mavmulcl  21880  m2detleiblem3  21962  m2detleiblem4  21963  iinopn  22235  ordtrest2  22539  iscnp2  22574  discmp  22733  2ndcdisj  22791  ptunimpt  22930  pttopon  22931  ptcnplem  22956  upxp  22958  txdis1cn  22970  cnmpt11  22998  cnmpt21  23006  cnmptkp  23015  cnmptk1  23016  cnmpt1k  23017  cnmptkk  23018  cnmptk1p  23020  qtopeu  23051  uzrest  23232  txflf  23341  clsnsg  23445  tgpconncomp  23448  tsmsf1o  23480  prdsmet  23707  fsumcn  24217  cncfmpt1f  24261  iccpnfcnv  24291  lebnumlem1  24308  copco  24365  pcoass  24371  bcth3  24679  voliun  24902  i1f1lem  25037  iblcnlem  25137  limcvallem  25219  ellimc2  25225  cnmptlimc  25238  dvle  25355  dvfsumle  25369  dvfsumge  25370  dvfsumabs  25371  dvfsumlem2  25375  itgsubstlem  25396  sincn  25787  coscn  25788  rlimcxp  26307  harmonicbnd  26337  harmonicbnd2  26338  lgamgulmlem6  26367  sqff1o  26515  lgseisenlem3  26709  fmptdF  31458  ordtrest2NEW  32373  ddemeas  32704  eulerpartgbij  32841  0rrv  32920  reprpmtf1o  33108  subfacf  33638  tailf  34814  fdc  36171  heiborlem5  36241  3factsumint  40449  dvle2  40496  elrfirn2  40957  mptfcl  40981  mzpexpmpt  41006  mzpsubst  41009  rabdiophlem1  41062  rabdiophlem2  41063  pw2f1ocnv  41299  refsumcn  43177  fompt  43347  fmptf  43401  fmptff  43435  fprodcnlem  43772  dvsinax  44086  itgsubsticclem  44148  fargshiftf  45564  isomuspgrlem2b  45953
  Copyright terms: Public domain W3C validator