Theorem fconst 6769

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 5721	. . 3 ⊢ (𝐴 × {𝐵}) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	1, 2	fnmpti 6686	. 2 ⊢ (𝐴 × {𝐵}) Fn 𝐴
4		rnxpss 6166	. 2 ⊢ ran (𝐴 × {𝐵}) ⊆ {𝐵}
5		df-f 6540	. 2 ⊢ ((𝐴 × {𝐵}):𝐴⟶{𝐵} ↔ ((𝐴 × {𝐵}) Fn 𝐴 ∧ ran (𝐴 × {𝐵}) ⊆ {𝐵}))
6	3, 4, 5	mpbir2an 711	1 ⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵}

Syntax hints:   ∈ wcel 2109  Vcvv 3464   ⊆ wss 3931  {csn 4606   × cxp 5657  ran crn 5660   Fn wfn 6531  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  fconstg  6770  fodomr  9147  fodomfir  9345  ofsubeq0  12242  ser0f  14078  hashgval  14356  hashinf  14358  hashfxnn0  14360  prodf1f  15913  pwssplit1  21022  psrbag0  22025  xkofvcn  23627  rrx0el  25355  ibl0  25745  dvcmul  25904  dvcmulf  25905  dvexp  25914  elqaalem3  26286  basellem7  27054  basellem9  27056  noetasuplem4  27705  axlowdimlem8  28933  axlowdimlem9  28934  axlowdimlem10  28935  axlowdimlem11  28936  axlowdimlem12  28937  0oo  30775  occllem  31289  ho01i  31814  nlelchi  32047  hmopidmchi  32137  elrgspnlem1  33242  eulerpartlemt  34408  plymul02  34583  breprexpnat  34671  fullfunfnv  35969  fullfunfv  35970  poimirlem16  37665  poimirlem19  37668  poimirlem23  37672  poimirlem24  37673  poimirlem25  37674  poimirlem28  37677  poimirlem29  37678  poimirlem30  37679  poimirlem31  37680  poimirlem32  37681  ftc1anclem5  37726  lfl0f  39092  diophrw  42749  pwssplit4  43080  ofsubid  44315  dvsconst  44321  dvsid  44322  binomcxplemnn0  44340  binomcxplemnotnn0  44347  functermc  49360  aacllem  49632