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

Theorem fmpt 7130
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 6708 . . 3 (∀𝑥𝐴 𝐶𝐵𝐹 Fn 𝐴)
31rnmpt 5968 . . . 4 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶}
4 r19.29 3114 . . . . . . 7 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → ∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶))
5 eleq1 2829 . . . . . . . . 9 (𝑦 = 𝐶 → (𝑦𝐵𝐶𝐵))
65biimparc 479 . . . . . . . 8 ((𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
76rexlimivw 3151 . . . . . . 7 (∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
84, 7syl 17 . . . . . 6 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → 𝑦𝐵)
98ex 412 . . . . 5 (∀𝑥𝐴 𝐶𝐵 → (∃𝑥𝐴 𝑦 = 𝐶𝑦𝐵))
109abssdv 4068 . . . 4 (∀𝑥𝐴 𝐶𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶} ⊆ 𝐵)
113, 10eqsstrid 4022 . . 3 (∀𝑥𝐴 𝐶𝐵 → ran 𝐹𝐵)
12 df-f 6565 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
132, 11, 12sylanbrc 583 . 2 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
14 fimacnv 6758 . . . 4 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐴)
151mptpreima 6258 . . . 4 (𝐹𝐵) = {𝑥𝐴𝐶𝐵}
1614, 15eqtr3di 2792 . . 3 (𝐹:𝐴𝐵𝐴 = {𝑥𝐴𝐶𝐵})
17 rabid2 3470 . . 3 (𝐴 = {𝑥𝐴𝐶𝐵} ↔ ∀𝑥𝐴 𝐶𝐵)
1816, 17sylib 218 . 2 (𝐹:𝐴𝐵 → ∀𝑥𝐴 𝐶𝐵)
1913, 18impbii 209 1 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wcel 2108  {cab 2714  wral 3061  wrex 3070  {crab 3436  wss 3951  cmpt 5225  ccnv 5684  ran crn 5686  cima 5688   Fn wfn 6556  wf 6557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-fun 6563  df-fn 6564  df-f 6565
This theorem is referenced by:  f1ompt  7131  fmpti  7132  fvmptelcdm  7133  fmptd  7134  fmptdf  7137  fompt  7138  rnmptss  7143  f1oresrab  7147  idref  7166  f1mpt  7281  f1stres  8038  f2ndres  8039  fmpox  8092  fmpoco  8120  onoviun  8383  onnseq  8384  mptelixpg  8975  dom2lem  9032  iinfi  9457  cantnfrescl  9716  acni2  10086  acnlem  10088  dfac4  10162  dfacacn  10182  fin23lem28  10380  axdc2lem  10488  axcclem  10497  ac6num  10519  uzf  12881  ccatalpha  14631  repsf  14811  rlim2  15532  rlimi  15549  o1fsum  15849  ackbijnn  15864  pcmptcl  16929  vdwlem11  17029  ismon2  17778  isepi2  17785  yonedalem3b  18324  smndex1gbas  18915  efgsf  19747  gsummhm2  19957  gsummptcl  19985  gsummptfif1o  19986  gsummptfzcl  19987  gsumcom2  19993  gsummptnn0fz  20004  issrngd  20856  ipcl  21651  subrgasclcl  22091  evl1sca  22338  mavmulcl  22553  m2detleiblem3  22635  m2detleiblem4  22636  iinopn  22908  ordtrest2  23212  iscnp2  23247  discmp  23406  2ndcdisj  23464  ptunimpt  23603  pttopon  23604  ptcnplem  23629  upxp  23631  txdis1cn  23643  cnmpt11  23671  cnmpt21  23679  cnmptkp  23688  cnmptk1  23689  cnmpt1k  23690  cnmptkk  23691  cnmptk1p  23693  qtopeu  23724  uzrest  23905  txflf  24014  clsnsg  24118  tgpconncomp  24121  tsmsf1o  24153  prdsmet  24380  fsumcn  24894  cncfmpt1f  24940  iccpnfcnv  24975  lebnumlem1  24993  copco  25051  pcoass  25057  bcth3  25365  voliun  25589  i1f1lem  25724  iblcnlem  25824  limcvallem  25906  ellimc2  25912  cnmptlimc  25925  dvle  26046  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgsubstlem  26089  sincn  26488  coscn  26489  rlimcxp  27017  harmonicbnd  27047  harmonicbnd2  27048  lgamgulmlem6  27077  sqff1o  27225  lgseisenlem3  27421  fmptdF  32666  ordtrest2NEW  33922  ddemeas  34237  eulerpartgbij  34374  0rrv  34453  reprpmtf1o  34641  subfacf  35180  tailf  36376  fdc  37752  heiborlem5  37822  3factsumint  42026  dvle2  42073  fmpocos  42275  elrfirn2  42707  mptfcl  42731  mzpexpmpt  42756  mzpsubst  42759  rabdiophlem1  42812  rabdiophlem2  42813  pw2f1ocnv  43049  refsumcn  45035  fmptf  45245  fmptff  45276  fprodcnlem  45614  dvsinax  45928  itgsubsticclem  45990  fargshiftf  47427
  Copyright terms: Public domain W3C validator