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

Theorem fmpt 6544
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 6181 . . 3 (∀𝑥𝐴 𝐶𝐵𝐹 Fn 𝐴)
31rnmpt 5526 . . . 4 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶}
4 r19.29 3210 . . . . . . 7 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → ∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶))
5 eleq1 2827 . . . . . . . . 9 (𝑦 = 𝐶 → (𝑦𝐵𝐶𝐵))
65biimparc 505 . . . . . . . 8 ((𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
76rexlimivw 3167 . . . . . . 7 (∃𝑥𝐴 (𝐶𝐵𝑦 = 𝐶) → 𝑦𝐵)
84, 7syl 17 . . . . . 6 ((∀𝑥𝐴 𝐶𝐵 ∧ ∃𝑥𝐴 𝑦 = 𝐶) → 𝑦𝐵)
98ex 449 . . . . 5 (∀𝑥𝐴 𝐶𝐵 → (∃𝑥𝐴 𝑦 = 𝐶𝑦𝐵))
109abssdv 3817 . . . 4 (∀𝑥𝐴 𝐶𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐶} ⊆ 𝐵)
113, 10syl5eqss 3790 . . 3 (∀𝑥𝐴 𝐶𝐵 → ran 𝐹𝐵)
12 df-f 6053 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
132, 11, 12sylanbrc 701 . 2 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
141mptpreima 5789 . . . 4 (𝐹𝐵) = {𝑥𝐴𝐶𝐵}
15 fimacnv 6510 . . . 4 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐴)
1614, 15syl5reqr 2809 . . 3 (𝐹:𝐴𝐵𝐴 = {𝑥𝐴𝐶𝐵})
17 rabid2 3257 . . 3 (𝐴 = {𝑥𝐴𝐶𝐵} ↔ ∀𝑥𝐴 𝐶𝐵)
1816, 17sylib 208 . 2 (𝐹:𝐴𝐵 → ∀𝑥𝐴 𝐶𝐵)
1913, 18impbii 199 1 (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1632  wcel 2139  {cab 2746  wral 3050  wrex 3051  {crab 3054  wss 3715  cmpt 4881  ccnv 5265  ran crn 5267  cima 5269   Fn wfn 6044  wf 6045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057
This theorem is referenced by:  f1ompt  6545  fmpti  6546  mptex2  6547  fmptd  6548  fmptdf  6550  rnmptss  6555  f1oresrab  6558  idref  6662  f1mpt  6681  f1stres  7357  f2ndres  7358  fmpt2x  7404  fmpt2co  7428  onoviun  7609  onnseq  7610  mptelixpg  8111  dom2lem  8161  iinfi  8488  cantnfrescl  8746  acni2  9059  acnlem  9061  dfac4  9135  dfacacn  9155  fin23lem28  9354  axdc2lem  9462  axcclem  9471  ac6num  9493  uzf  11882  ccatalpha  13565  repsf  13720  rlim2  14426  rlimi  14443  rlimmptrcl  14537  lo1mptrcl  14551  o1mptrcl  14552  o1fsum  14744  ackbijnn  14759  pcmptcl  15797  vdwlem11  15897  ismon2  16595  isepi2  16602  yonedalem3b  17120  efgsf  18342  gsummhm2  18539  gsummptcl  18566  gsummptfif1o  18567  gsummptfzcl  18568  gsumcom2  18574  gsummptnn0fz  18582  issrngd  19063  psrass1lem  19579  subrgasclcl  19701  evl1sca  19900  ipcl  20180  frlmgsum  20313  uvcresum  20334  mavmulcl  20555  m2detleiblem3  20637  m2detleiblem4  20638  iinopn  20909  ordtrest2  21210  iscnp2  21245  discmp  21403  2ndcdisj  21461  ptunimpt  21600  pttopon  21601  txcnp  21625  ptcnplem  21626  ptcnp  21627  upxp  21628  ptcn  21632  txdis1cn  21640  cnmpt11  21668  cnmpt1t  21670  cnmpt12  21672  cnmpt21  21676  cnmptkp  21685  cnmptk1  21686  cnmpt1k  21687  cnmptkk  21688  cnmptk1p  21690  cnmptk2  21691  qtopeu  21721  uzrest  21902  txflf  22011  cnmpt1plusg  22092  clsnsg  22114  tgpconncomp  22117  tsmsf1o  22149  cnmpt1vsca  22198  prdsmet  22376  cnmpt1ds  22846  fsumcn  22874  cncfmpt1f  22917  cncfmpt2ss  22919  iccpnfcnv  22944  lebnumlem1  22961  copco  23018  pcoass  23024  cnmpt1ip  23246  bcth3  23328  voliun  23522  mbfmptcl  23603  i1f1lem  23655  i1fposd  23673  iblcnlem  23754  itgss3  23780  limcvallem  23834  ellimc2  23840  cnmptlimc  23853  dvmptcl  23921  dvmptco  23934  dvle  23969  dvfsumle  23983  dvfsumge  23984  dvfsumabs  23985  dvmptrecl  23986  dvfsumlem2  23989  itgparts  24009  itgsubstlem  24010  itgsubst  24011  ulmss  24350  ulmdvlem2  24354  itgulm2  24362  sincn  24397  coscn  24398  logtayl  24605  rlimcxp  24899  harmonicbnd  24929  harmonicbnd2  24930  lgamgulmlem6  24959  sqff1o  25107  lgseisenlem3  25301  fmptdF  29765  ordtrest2NEW  30278  ddemeas  30608  eulerpartgbij  30743  0rrv  30822  reprpmtf1o  31013  subfacf  31464  tailf  32676  fdc  33854  heiborlem5  33927  elrfirn2  37761  mptfcl  37785  mzpexpmpt  37810  mzpsubst  37813  rabdiophlem1  37867  rabdiophlem2  37868  pw2f1ocnv  38106  refsumcn  39688  fompt  39878  fvmptelrn  39927  fmptf  39947  fprodcnlem  40334  dvsinax  40630  itgsubsticclem  40694  fargshiftf  41886
  Copyright terms: Public domain W3C validator