Theorem fconst 6764

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3904  {csn 4588   × cxp 5659  ran crn 5662   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 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  fconstg  6765  fodomr  9115  fodomfir  9286  ofsubeq0  12214  ser0f  14090  hashgval  14368  hashinf  14370  hashfxnn0  14372  prodf1f  15945  pwssplit1  21159  psrbag0  22192  xkofvcn  23820  rrx0el  25536  ibl0  25925  dvcmul  26082  dvcmulf  26083  dvexp  26091  plymul02  26420  elqaalem3  26461  basellem7  27227  basellem9  27229  noetasuplem4  27876  axlowdimlem8  29265  axlowdimlem9  29266  axlowdimlem10  29267  axlowdimlem11  29268  axlowdimlem12  29269  0oo  31107  occllem  31621  ho01i  32146  nlelchi  32379  hmopidmchi  32469  elrgspnlem1  33528  gsumind  33631  esplyfval0  33920  eulerpartlemt  34727  breprexpnat  34987  fullfunfnv  36392  fullfunfv  36393  poimirlem16  38231  poimirlem19  38234  poimirlem23  38238  poimirlem24  38239  poimirlem25  38240  poimirlem28  38243  poimirlem29  38244  poimirlem30  38245  poimirlem31  38246  poimirlem32  38247  ftc1anclem5  38292  lfl0f  39789  diophrw  43438  pwssplit4  43764  ofsubid  44982  dvsconst  44988  dvsid  44989  binomcxplemnn0  45007  binomcxplemnotnn0  45014  functermc  50231  aacllem  50546