Theorem fconst 6721

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.

Step	Hyp	Ref	Expression
1		fconst.1	. . 3 ⊢ 𝐵 ∈ V
2		fconstmpt 5687	. . 3 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	1, 2	fnmpti 6636	. 2 ⊢ (𝐴 × {𝐵}) Fn 𝐴
4		rnxpss 6131	. 2 ⊢ ran (𝐴 × {𝐵}) ⊆ {𝐵}
5		df-f 6497	. 2 ⊢ ((𝐴 × {𝐵}):𝐴⟶{𝐵} ↔ ((𝐴 × {𝐵}) Fn 𝐴 ∧ ran (𝐴 × {𝐵}) ⊆ {𝐵}))
6	3, 4, 5	mpbir2an 712	1 ⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵}

Syntax hints:   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902  {csn 4581   × cxp 5623  ran crn 5626   Fn wfn 6488  ⟶wf 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6495  df-fn 6496  df-f 6497

This theorem is referenced by:  fconstg  6722  fodomr  9061  fodomfir  9233  ofsubeq0  12147  ser0f  13983  hashgval  14261  hashinf  14263  hashfxnn0  14265  prodf1f  15820  pwssplit1  21016  psrbag0  22022  xkofvcn  23633  rrx0el  25359  ibl0  25749  dvcmul  25908  dvcmulf  25909  dvexp  25918  elqaalem3  26290  basellem7  27058  basellem9  27060  noetasuplem4  27709  axlowdimlem8  29027  axlowdimlem9  29028  axlowdimlem10  29029  axlowdimlem11  29030  axlowdimlem12  29031  0oo  30869  occllem  31383  ho01i  31908  nlelchi  32141  hmopidmchi  32231  elrgspnlem1  33328  gsumind  33430  esplyfval0  33733  eulerpartlemt  34541  plymul02  34716  breprexpnat  34804  fullfunfnv  36153  fullfunfv  36154  poimirlem16  37850  poimirlem19  37853  poimirlem23  37857  poimirlem24  37858  poimirlem25  37859  poimirlem28  37862  poimirlem29  37863  poimirlem30  37864  poimirlem31  37865  poimirlem32  37866  ftc1anclem5  37911  lfl0f  39408  diophrw  43079  pwssplit4  43409  ofsubid  44643  dvsconst  44649  dvsid  44650  binomcxplemnn0  44668  binomcxplemnotnn0  44675  functermc  49830  aacllem  50123