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

Theorem fmpt 6421
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 6058 . . 3 (∀𝑥𝐴 𝐶𝐵𝐹 Fn 𝐴)
31rnmpt 5403 . . . 4 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶}
4 r19.29 3101 . . . . . . 7 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → ∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶))
5 eleq1 2718 . . . . . . . . 9 (𝑦 = 𝐶 → (𝑦𝐵𝐶𝐵))
65biimparc 503 . . . . . . . 8 ((𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
76rexlimivw 3058 . . . . . . 7 (∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
84, 7syl 17 . . . . . 6 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → 𝑦𝐵)
98ex 449 . . . . 5 (∀𝑥𝐴 𝐶𝐵 → (∃𝑥𝐴 𝑦 = 𝐶𝑦𝐵))
109abssdv 3709 . . . 4 (∀𝑥𝐴 𝐶𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶} ⊆ 𝐵)
113, 10syl5eqss 3682 . . 3 (∀𝑥𝐴 𝐶𝐵 → ran 𝐹𝐵)
12 df-f 5930 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
132, 11, 12sylanbrc 699 . 2 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
141mptpreima 5666 . . . 4 (𝐹𝐵) = {𝑥𝐴𝐶𝐵}
15 fimacnv 6387 . . . 4 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐴)
1614, 15syl5reqr 2700 . . 3 (𝐹:𝐴𝐵𝐴 = {𝑥𝐴𝐶𝐵})
17 rabid2 3148 . . 3 (𝐴 = {𝑥𝐴𝐶𝐵} ↔ ∀𝑥𝐴 𝐶𝐵)
1816, 17sylib 208 . 2 (𝐹:𝐴𝐵 → ∀𝑥𝐴 𝐶𝐵)
1913, 18impbii 199 1 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1523  wcel 2030  {cab 2637  wral 2941  wrex 2942  {crab 2945  wss 3607  cmpt 4762  ccnv 5142  ran crn 5144  cima 5146   Fn wfn 5921  wf 5922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934
This theorem is referenced by:  f1ompt  6422  fmpti  6423  mptex2  6424  fmptd  6425  fmptdf  6427  rnmptss  6432  f1oresrab  6435  idref  6539  f1mpt  6558  f1stres  7234  f2ndres  7235  fmpt2x  7281  fmpt2co  7305  onoviun  7485  onnseq  7486  mptelixpg  7987  dom2lem  8037  iinfi  8364  cantnfrescl  8611  acni2  8907  acnlem  8909  dfac4  8983  dfacacn  9001  fin23lem28  9200  axdc2lem  9308  axcclem  9317  ac6num  9339  uzf  11728  ccatalpha  13411  repsf  13566  rlim2  14271  rlimi  14288  rlimmptrcl  14382  lo1mptrcl  14396  o1mptrcl  14397  o1fsum  14589  ackbijnn  14604  pcmptcl  15642  vdwlem11  15742  ismon2  16441  isepi2  16448  yonedalem3b  16966  efgsf  18188  gsummhm2  18385  gsummptcl  18412  gsummptfif1o  18413  gsummptfzcl  18414  gsumcom2  18420  gsummptnn0fz  18428  issrngd  18909  psrass1lem  19425  subrgasclcl  19547  evl1sca  19746  ipcl  20026  frlmgsum  20159  uvcresum  20180  mavmulcl  20401  m2detleiblem3  20483  m2detleiblem4  20484  iinopn  20755  ordtrest2  21056  iscnp2  21091  discmp  21249  2ndcdisj  21307  ptunimpt  21446  pttopon  21447  txcnp  21471  ptcnplem  21472  ptcnp  21473  upxp  21474  ptcn  21478  txdis1cn  21486  cnmpt11  21514  cnmpt1t  21516  cnmpt12  21518  cnmpt21  21522  cnmptkp  21531  cnmptk1  21532  cnmpt1k  21533  cnmptkk  21534  cnmptk1p  21536  cnmptk2  21537  qtopeu  21567  uzrest  21748  txflf  21857  cnmpt1plusg  21938  clsnsg  21960  tgpconncomp  21963  tsmsf1o  21995  cnmpt1vsca  22044  prdsmet  22222  cnmpt1ds  22692  fsumcn  22720  cncfmpt1f  22763  cncfmpt2ss  22765  iccpnfcnv  22790  lebnumlem1  22807  copco  22864  pcoass  22870  cnmpt1ip  23092  bcth3  23174  voliun  23368  mbfmptcl  23449  i1f1lem  23501  i1fposd  23519  iblcnlem  23600  itgss3  23626  limcvallem  23680  ellimc2  23686  cnmptlimc  23699  dvmptcl  23767  dvmptco  23780  dvle  23815  dvfsumle  23829  dvfsumge  23830  dvfsumabs  23831  dvmptrecl  23832  dvfsumlem2  23835  itgparts  23855  itgsubstlem  23856  itgsubst  23857  ulmss  24196  ulmdvlem2  24200  itgulm2  24208  sincn  24243  coscn  24244  logtayl  24451  rlimcxp  24745  harmonicbnd  24775  harmonicbnd2  24776  lgamgulmlem6  24805  sqff1o  24953  lgseisenlem3  25147  fmptdF  29584  ordtrest2NEW  30097  ddemeas  30427  eulerpartgbij  30562  0rrv  30641  reprpmtf1o  30832  subfacf  31283  tailf  32495  fdc  33671  heiborlem5  33744  elrfirn2  37576  mptfcl  37600  mzpexpmpt  37625  mzpsubst  37628  rabdiophlem1  37682  rabdiophlem2  37683  pw2f1ocnv  37921  refsumcn  39503  fompt  39693  fvmptelrn  39742  fmptf  39762  fprodcnlem  40149  dvsinax  40445  itgsubsticclem  40509  fargshiftf  41701
  Copyright terms: Public domain W3C validator