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

Theorem fmpt 7058
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 6641 . . 3 (∀𝑥𝐴 𝐶𝐵𝐹 Fn 𝐴)
31rnmpt 5910 . . . 4 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶}
4 r19.29 3117 . . . . . . 7 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → ∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶))
5 eleq1 2825 . . . . . . . . 9 (𝑦 = 𝐶 → (𝑦𝐵𝐶𝐵))
65biimparc 480 . . . . . . . 8 ((𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
76rexlimivw 3148 . . . . . . 7 (∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
84, 7syl 17 . . . . . 6 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → 𝑦𝐵)
98ex 413 . . . . 5 (∀𝑥𝐴 𝐶𝐵 → (∃𝑥𝐴 𝑦 = 𝐶𝑦𝐵))
109abssdv 4025 . . . 4 (∀𝑥𝐴 𝐶𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶} ⊆ 𝐵)
113, 10eqsstrid 3992 . . 3 (∀𝑥𝐴 𝐶𝐵 → ran 𝐹𝐵)
12 df-f 6500 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
132, 11, 12sylanbrc 583 . 2 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
14 fimacnv 6690 . . . 4 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐴)
151mptpreima 6190 . . . 4 (𝐹𝐵) = {𝑥𝐴𝐶𝐵}
1614, 15eqtr3di 2791 . . 3 (𝐹:𝐴𝐵𝐴 = {𝑥𝐴𝐶𝐵})
17 rabid2 3436 . . 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 3064  wrex 3073  {crab 3407  wss 3910  cmpt 5188  ccnv 5632  ran crn 5634  cima 5636   Fn wfn 6491  wf 6492
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 5256  ax-nul 5263  ax-pr 5384
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 2889  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-fun 6498  df-fn 6499  df-f 6500
This theorem is referenced by:  f1ompt  7059  fmpti  7060  fvmptelcdm  7061  fmptd  7062  fmptdf  7065  rnmptss  7070  f1oresrab  7073  idref  7092  f1mpt  7208  f1stres  7945  f2ndres  7946  fmpox  7999  fmpoco  8027  onoviun  8289  onnseq  8290  mptelixpg  8873  dom2lem  8932  iinfi  9353  cantnfrescl  9612  acni2  9982  acnlem  9984  dfac4  10058  dfacacn  10077  fin23lem28  10276  axdc2lem  10384  axcclem  10393  ac6num  10415  uzf  12766  ccatalpha  14481  repsf  14661  rlim2  15378  rlimi  15395  o1fsum  15698  ackbijnn  15713  pcmptcl  16763  vdwlem11  16863  ismon2  17617  isepi2  17624  yonedalem3b  18168  smndex1gbas  18712  efgsf  19511  gsummhm2  19716  gsummptcl  19744  gsummptfif1o  19745  gsummptfzcl  19746  gsumcom2  19752  gsummptnn0fz  19763  issrngd  20320  ipcl  21037  subrgasclcl  21475  evl1sca  21700  mavmulcl  21896  m2detleiblem3  21978  m2detleiblem4  21979  iinopn  22251  ordtrest2  22555  iscnp2  22590  discmp  22749  2ndcdisj  22807  ptunimpt  22946  pttopon  22947  ptcnplem  22972  upxp  22974  txdis1cn  22986  cnmpt11  23014  cnmpt21  23022  cnmptkp  23031  cnmptk1  23032  cnmpt1k  23033  cnmptkk  23034  cnmptk1p  23036  qtopeu  23067  uzrest  23248  txflf  23357  clsnsg  23461  tgpconncomp  23464  tsmsf1o  23496  prdsmet  23723  fsumcn  24233  cncfmpt1f  24277  iccpnfcnv  24307  lebnumlem1  24324  copco  24381  pcoass  24387  bcth3  24695  voliun  24918  i1f1lem  25053  iblcnlem  25153  limcvallem  25235  ellimc2  25241  cnmptlimc  25254  dvle  25371  dvfsumle  25385  dvfsumge  25386  dvfsumabs  25387  dvfsumlem2  25391  itgsubstlem  25412  sincn  25803  coscn  25804  rlimcxp  26323  harmonicbnd  26353  harmonicbnd2  26354  lgamgulmlem6  26383  sqff1o  26531  lgseisenlem3  26725  fmptdF  31572  ordtrest2NEW  32504  ddemeas  32835  eulerpartgbij  32972  0rrv  33051  reprpmtf1o  33239  subfacf  33769  tailf  34847  fdc  36204  heiborlem5  36274  3factsumint  40482  dvle2  40529  elrfirn2  41005  mptfcl  41029  mzpexpmpt  41054  mzpsubst  41057  rabdiophlem1  41110  rabdiophlem2  41111  pw2f1ocnv  41347  refsumcn  43225  fompt  43401  fmptf  43455  fmptff  43488  fprodcnlem  43830  dvsinax  44144  itgsubsticclem  44206  fargshiftf  45622  isomuspgrlem2b  46011
  Copyright terms: Public domain W3C validator