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

Theorem fconst 6561
Description: A Cartesian 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 𝐵 ∈ V
Assertion
Ref Expression
fconst (𝐴 × {𝐵}):𝐴⟶{𝐵}

Proof of Theorem fconst
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fconst.1 . . 3 𝐵 ∈ V
2 fconstmpt 5612 . . 3 (𝐴 × {𝐵}) = (𝑥𝐴𝐵)
31, 2fnmpti 6487 . 2 (𝐴 × {𝐵}) Fn 𝐴
4 rnxpss 6026 . 2 ran (𝐴 × {𝐵}) ⊆ {𝐵}
5 df-f 6355 . 2 ((𝐴 × {𝐵}):𝐴⟶{𝐵} ↔ ((𝐴 × {𝐵}) Fn 𝐴 ∧ ran (𝐴 × {𝐵}) ⊆ {𝐵}))
63, 4, 5mpbir2an 707 1 (𝐴 × {𝐵}):𝐴⟶{𝐵}
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3499  wss 3939  {csn 4563   × cxp 5551  ran crn 5554   Fn wfn 6346  wf 6347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pr 5325
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-fun 6353  df-fn 6354  df-f 6355
This theorem is referenced by:  fconstg  6562  fodomr  8660  ofsubeq0  11627  ser0f  13416  hashgval  13686  hashinf  13688  hashfxnn0  13690  prodf1f  15240  pwssplit1  19753  psrbag0  20194  xkofvcn  22210  rrx0el  23918  ibl0  24304  dvcmul  24458  dvcmulf  24459  dvexp  24467  elqaalem3  24827  basellem7  25580  basellem9  25582  axlowdimlem8  26651  axlowdimlem9  26652  axlowdimlem10  26653  axlowdimlem11  26654  axlowdimlem12  26655  0oo  28482  occllem  28996  ho01i  29521  nlelchi  29754  hmopidmchi  29844  eulerpartlemt  31517  plymul02  31704  breprexpnat  31793  noetalem3  33105  fullfunfnv  33293  fullfunfv  33294  poimirlem16  34777  poimirlem19  34780  poimirlem23  34784  poimirlem24  34785  poimirlem25  34786  poimirlem28  34789  poimirlem29  34790  poimirlem30  34791  poimirlem31  34792  poimirlem32  34793  ftc1anclem5  34840  lfl0f  36074  diophrw  39223  pwssplit4  39556  ofsubid  40523  dvsconst  40529  dvsid  40530  binomcxplemnn0  40548  binomcxplemnotnn0  40555  aacllem  44736
  Copyright terms: Public domain W3C validator