MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fconst Unicode version

Theorem fconst 5510
Description: A cross product with a singleton is a constant function. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Hypothesis
Ref Expression
fconst.1  |-  B  e. 
_V
Assertion
Ref Expression
fconst  |-  ( A  X.  { B }
) : A --> { B }

Proof of Theorem fconst
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 fconst.1 . . 3  |-  B  e. 
_V
2 fconstmpt 4814 . . 3  |-  ( A  X.  { B }
)  =  ( x  e.  A  |->  B )
31, 2fnmpti 5454 . 2  |-  ( A  X.  { B }
)  Fn  A
4 rnxpss 5190 . 2  |-  ran  ( A  X.  { B }
)  C_  { B }
5 df-f 5341 . 2  |-  ( ( A  X.  { B } ) : A --> { B }  <->  ( ( A  X.  { B }
)  Fn  A  /\  ran  ( A  X.  { B } )  C_  { B } ) )
63, 4, 5mpbir2an 886 1  |-  ( A  X.  { B }
) : A --> { B }
Colors of variables: wff set class
Syntax hints:    e. wcel 1710   _Vcvv 2864    C_ wss 3228   {csn 3716    X. cxp 4769   ran crn 4772    Fn wfn 5332   -->wf 5333
This theorem is referenced by:  fconstg  5511  fodomr  7100  ofsubeq0  9833  ser0f  11191  hashgval  11433  hashinf  11435  hashf  11437  psrbag0  16334  xkofvcn  17484  ibl0  19245  dvcmul  19397  dvcmulf  19398  dvexp  19406  elqaalem3  19805  basellem7  20436  basellem9  20438  0oo  21481  occllem  21996  ho01i  22522  nlelchi  22755  hmopidmchi  22845  prodf1f  24521  fullfunfnv  25043  fullfunfv  25044  axlowdimlem8  25136  axlowdimlem9  25137  axlowdimlem10  25138  axlowdimlem11  25139  axlowdimlem12  25140  itg2addnclem  25492  itg2addnc  25494  diophrw  26161  pwssplit1  26511  pwssplit4  26514  ofsubid  26864  dvsconst  26870  dvsid  26871  lfl0f  29328
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-fun 5339  df-fn 5340  df-f 5341
  Copyright terms: Public domain W3C validator