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

Theorem fmpt 6574
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 6200 . . 3 (∀𝑥𝐴 𝐶𝐵𝐹 Fn 𝐴)
31rnmpt 5542 . . . 4 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶}
4 r19.29 3219 . . . . . . 7 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → ∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶))
5 eleq1 2832 . . . . . . . . 9 (𝑦 = 𝐶 → (𝑦𝐵𝐶𝐵))
65biimparc 471 . . . . . . . 8 ((𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
76rexlimivw 3176 . . . . . . 7 (∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
84, 7syl 17 . . . . . 6 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → 𝑦𝐵)
98ex 401 . . . . 5 (∀𝑥𝐴 𝐶𝐵 → (∃𝑥𝐴 𝑦 = 𝐶𝑦𝐵))
109abssdv 3838 . . . 4 (∀𝑥𝐴 𝐶𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶} ⊆ 𝐵)
113, 10syl5eqss 3811 . . 3 (∀𝑥𝐴 𝐶𝐵 → ran 𝐹𝐵)
12 df-f 6074 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
132, 11, 12sylanbrc 578 . 2 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
141mptpreima 5816 . . . 4 (𝐹𝐵) = {𝑥𝐴𝐶𝐵}
15 fimacnv 6541 . . . 4 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐴)
1614, 15syl5reqr 2814 . . 3 (𝐹:𝐴𝐵𝐴 = {𝑥𝐴𝐶𝐵})
17 rabid2 3266 . . 3 (𝐴 = {𝑥𝐴𝐶𝐵} ↔ ∀𝑥𝐴 𝐶𝐵)
1816, 17sylib 209 . 2 (𝐹:𝐴𝐵 → ∀𝑥𝐴 𝐶𝐵)
1913, 18impbii 200 1 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1652  wcel 2155  {cab 2751  wral 3055  wrex 3056  {crab 3059  wss 3734  cmpt 4890  ccnv 5278  ran crn 5280  cima 5282   Fn wfn 6065  wf 6066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3599  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-fv 6078
This theorem is referenced by:  f1ompt  6575  fmpti  6576  fvmptelrn  6577  fmptd  6578  fmptdf  6581  rnmptss  6586  f1oresrab  6589  idref  6607  f1mpt  6714  f1stres  7394  f2ndres  7395  fmpt2x  7441  fmpt2co  7466  onoviun  7648  onnseq  7649  mptelixpg  8154  dom2lem  8204  iinfi  8534  cantnfrescl  8792  acni2  9124  acnlem  9126  dfac4  9200  dfacacn  9220  fin23lem28  9419  axdc2lem  9527  axcclem  9536  ac6num  9558  uzf  11894  ccatalpha  13570  repsf  13811  rlim2  14526  rlimi  14543  rlimmptrcl  14637  lo1mptrcl  14651  o1mptrcl  14652  o1fsum  14843  ackbijnn  14858  pcmptcl  15888  vdwlem11  15988  ismon2  16673  isepi2  16680  yonedalem3b  17199  efgsf  18420  gsummhm2  18619  gsummptcl  18646  gsummptfif1o  18647  gsummptfzcl  18648  gsumcom2  18654  gsummptnn0fz  18662  gsummptnn0fzOLD  18663  issrngd  19144  psrass1lem  19665  subrgasclcl  19786  evl1sca  19985  ipcl  20267  frlmgsum  20401  uvcresum  20422  mavmulcl  20644  m2detleiblem3  20726  m2detleiblem4  20727  iinopn  21000  ordtrest2  21302  iscnp2  21337  discmp  21495  2ndcdisj  21553  ptunimpt  21692  pttopon  21693  txcnp  21717  ptcnplem  21718  ptcnp  21719  upxp  21720  ptcn  21724  txdis1cn  21732  cnmpt11  21760  cnmpt1t  21762  cnmpt12  21764  cnmpt21  21768  cnmptkp  21777  cnmptk1  21778  cnmpt1k  21779  cnmptkk  21780  cnmptk1p  21782  cnmptk2  21783  qtopeu  21813  uzrest  21994  txflf  22103  cnmpt1plusg  22184  clsnsg  22206  tgpconncomp  22209  tsmsf1o  22241  cnmpt1vsca  22290  prdsmet  22468  cnmpt1ds  22938  fsumcn  22966  cncfmpt1f  23009  cncfmpt2ss  23011  iccpnfcnv  23036  lebnumlem1  23053  copco  23110  pcoass  23116  cnmpt1ip  23338  bcth3  23422  voliun  23626  mbfmptcl  23708  i1f1lem  23761  i1fposd  23779  iblcnlem  23860  itgss3  23886  limcvallem  23940  ellimc2  23946  cnmptlimc  23959  dvmptcl  24027  dvmptco  24040  dvle  24075  dvfsumle  24089  dvfsumge  24090  dvfsumabs  24091  dvmptrecl  24092  dvfsumlem2  24095  itgparts  24115  itgsubstlem  24116  itgsubst  24117  ulmss  24456  ulmdvlem2  24460  sincn  24503  coscn  24504  logtayl  24711  rlimcxp  25005  harmonicbnd  25035  harmonicbnd2  25036  lgamgulmlem6  25065  sqff1o  25213  lgseisenlem3  25407  fmptdF  29927  ordtrest2NEW  30437  ddemeas  30767  eulerpartgbij  30902  0rrv  30982  reprpmtf1o  31176  subfacf  31626  tailf  32834  fdc  33984  heiborlem5  34057  elrfirn2  37961  mptfcl  37985  mzpexpmpt  38010  mzpsubst  38013  rabdiophlem1  38067  rabdiophlem2  38068  pw2f1ocnv  38305  refsumcn  39865  fompt  40050  fmptf  40114  fprodcnlem  40493  dvsinax  40789  itgsubsticclem  40852  fargshiftf  42134
  Copyright terms: Public domain W3C validator