Theorem fconst 6768

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  {csn 4583   × cxp 5648  ran crn 5651   Fn wfn 6533  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  fconstg  6769  fodomr  9147  fodomfir  9319  ofsubeq0  12317  ser0f  14198  hashgval  14477  hashinf  14479  hashfxnn0  14481  prodf1f  16061  pwssplit1  21334  psrbag0  22371  xkofvcn  24003  rrx0el  25719  ibl0  26107  dvcmul  26264  dvcmulf  26265  dvexp  26273  plymul02  26601  elqaalem3  26644  basellem7  27414  basellem9  27416  noetasuplem4  28093  axlowdimlem8  29527  axlowdimlem9  29528  axlowdimlem10  29529  axlowdimlem11  29530  axlowdimlem12  29531  0oo  31391  occllem  31905  ho01i  32430  nlelchi  32663  hmopidmchi  32753  elrgspnlem1  33845  gsumind  33948  esplyfval0  34238  eulerpartlemt  35045  breprexpnat  35305  fullfunfnv  36752  fullfunfv  36753  poimirlem16  38597  poimirlem19  38600  poimirlem23  38604  poimirlem24  38605  poimirlem25  38606  poimirlem28  38609  poimirlem29  38610  poimirlem30  38611  poimirlem31  38612  poimirlem32  38613  ftc1anclem5  38658  lfl0f  40169  diophrw  43813  pwssplit4  44134  ofsubid  45351  dvsconst  45357  dvsid  45358  binomcxplemnn0  45376  binomcxplemnotnn0  45383  functermc  50659  aacllem  50982