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

Theorem fmpt 6337
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 5977 . . 3 (∀𝑥𝐴 𝐶𝐵𝐹 Fn 𝐴)
31rnmpt 5331 . . . 4 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶}
4 r19.29 3065 . . . . . . 7 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → ∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶))
5 eleq1 2686 . . . . . . . . 9 (𝑦 = 𝐶 → (𝑦𝐵𝐶𝐵))
65biimparc 504 . . . . . . . 8 ((𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
76rexlimivw 3022 . . . . . . 7 (∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
84, 7syl 17 . . . . . 6 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → 𝑦𝐵)
98ex 450 . . . . 5 (∀𝑥𝐴 𝐶𝐵 → (∃𝑥𝐴 𝑦 = 𝐶𝑦𝐵))
109abssdv 3655 . . . 4 (∀𝑥𝐴 𝐶𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶} ⊆ 𝐵)
113, 10syl5eqss 3628 . . 3 (∀𝑥𝐴 𝐶𝐵 → ran 𝐹𝐵)
12 df-f 5851 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
132, 11, 12sylanbrc 697 . 2 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
141mptpreima 5587 . . . 4 (𝐹𝐵) = {𝑥𝐴𝐶𝐵}
15 fimacnv 6303 . . . 4 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐴)
1614, 15syl5reqr 2670 . . 3 (𝐹:𝐴𝐵𝐴 = {𝑥𝐴𝐶𝐵})
17 rabid2 3107 . . 3 (𝐴 = {𝑥𝐴𝐶𝐵} ↔ ∀𝑥𝐴 𝐶𝐵)
1816, 17sylib 208 . 2 (𝐹:𝐴𝐵 → ∀𝑥𝐴 𝐶𝐵)
1913, 18impbii 199 1 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1480  wcel 1987  {cab 2607  wral 2907  wrex 2908  {crab 2911  wss 3555  cmpt 4673  ccnv 5073  ran crn 5075  cima 5077   Fn wfn 5842  wf 5843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fv 5855
This theorem is referenced by:  f1ompt  6338  fmpti  6339  fmptd  6340  fmptdf  6342  rnmptss  6347  f1oresrab  6350  idref  6453  f1mpt  6472  f1stres  7135  f2ndres  7136  fmpt2x  7181  fmpt2co  7205  onoviun  7385  onnseq  7386  mptelixpg  7889  dom2lem  7939  iinfi  8267  cantnfrescl  8517  acni2  8813  acnlem  8815  dfac4  8889  dfacacn  8907  fin23lem28  9106  axdc2lem  9214  axcclem  9223  ac6num  9245  uzf  11634  ccatalpha  13314  repsf  13457  rlim2  14161  rlimi  14178  rlimmptrcl  14272  lo1mptrcl  14286  o1mptrcl  14287  o1fsum  14472  ackbijnn  14485  pcmptcl  15519  vdwlem11  15619  ismon2  16315  isepi2  16322  yonedalem3b  16840  efgsf  18063  gsummhm2  18260  gsummptcl  18287  gsummptfif1o  18288  gsummptfzcl  18289  gsumcom2  18295  gsummptnn0fz  18303  issrngd  18782  psrass1lem  19296  subrgasclcl  19418  evl1sca  19617  ipcl  19897  frlmgsum  20030  uvcresum  20051  mavmulcl  20272  m2detleiblem3  20354  m2detleiblem4  20355  iinopn  20632  ordtrest2  20918  iscnp2  20953  discmp  21111  2ndcdisj  21169  ptunimpt  21308  pttopon  21309  txcnp  21333  ptcnplem  21334  ptcnp  21335  upxp  21336  ptcn  21340  txdis1cn  21348  cnmpt11  21376  cnmpt1t  21378  cnmpt12  21380  cnmpt21  21384  cnmptkp  21393  cnmptk1  21394  cnmpt1k  21395  cnmptkk  21396  cnmptk1p  21398  cnmptk2  21399  qtopeu  21429  uzrest  21611  txflf  21720  cnmpt1plusg  21801  clsnsg  21823  tgpconncomp  21826  tsmsf1o  21858  cnmpt1vsca  21907  prdsmet  22085  cnmpt1ds  22553  fsumcn  22581  cncfmpt1f  22624  cncfmpt2ss  22626  iccpnfcnv  22651  lebnumlem1  22668  copco  22726  pcoass  22732  cnmpt1ip  22954  bcth3  23036  voliun  23229  mbfmptcl  23310  i1f1lem  23362  i1fposd  23380  iblcnlem  23461  itgss3  23487  limcvallem  23541  ellimc2  23547  cnmptlimc  23560  dvmptcl  23628  dvmptco  23641  dvle  23674  dvfsumle  23688  dvfsumge  23689  dvfsumabs  23690  dvmptrecl  23691  dvfsumlem2  23694  itgparts  23714  itgsubstlem  23715  itgsubst  23716  ulmss  24055  ulmdvlem2  24059  itgulm2  24067  sincn  24102  coscn  24103  logtayl  24306  rlimcxp  24600  harmonicbnd  24630  harmonicbnd2  24631  lgamgulmlem6  24660  sqff1o  24808  lgseisenlem3  25002  fmptdF  29295  ordtrest2NEW  29748  ddemeas  30077  eulerpartgbij  30212  0rrv  30291  subfacf  30862  tailf  32009  fdc  33170  heiborlem5  33243  elrfirn2  36736  mptfcl  36760  mzpexpmpt  36785  mzpsubst  36788  rabdiophlem1  36842  rabdiophlem2  36843  pw2f1ocnv  37081  refsumcn  38669  mptex2  38820  fompt  38850  fvmptelrn  38899  fmptf  38920  fprodcnlem  39232  dvsinax  39429  itgsubsticclem  39495  fargshiftf  40671
  Copyright terms: Public domain W3C validator