Theorem fconst 3658

Description: A cross product with a singleton is a constant function.

Hypothesis

Ref	Expression
fconst.1	|- B e. V

Assertion

Ref	Expression
fconst	|- (A X. {B}):A-->{B}

Proof of Theorem fconst

Step	Hyp	Ref	Expression
1		f0 3656	. . 3 |- (/):(/)-->{B}
2		xpeq1 3200	. . . . . 6 |- (A = (/) -> (A X. {B}) = ((/) X. {B}))
3		xp0r 3239	. . . . . 6 |- ((/) X. {B}) = (/)
4	2, 3	syl6eq 1523	. . . . 5 |- (A = (/) -> (A X. {B}) = (/))
5	4	feq1d 3624	. . . 4 |- (A = (/) -> ((A X. {B}):A-->{B} <-> (/):A-->{B}))
6		feq2 3621	. . . 4 |- (A = (/) -> ((/):A-->{B} <-> (/):(/)-->{B}))
7	5, 6	bitrd 528	. . 3 |- (A = (/) -> ((A X. {B}):A-->{B} <-> (/):(/)-->{B}))
8	1, 7	mpbiri 194	. 2 |- (A = (/) -> (A X. {B}):A-->{B})
9		rnxp 3472	. . . . 5 |- (A =/= (/) -> ran ( A X. {B}) = {B})
10		eqimss 2109	. . . . 5 |- (ran ( A X. {B}) = {B} -> ran ( A X. {B}) (_ {B})
11	9, 10	syl 10	. . . 4 |- (A =/= (/) -> ran ( A X. {B}) (_ {B})
12		df-fn 3193	. . . . 5 |- ((A X. {B}) Fn A <-> (Fun (A X. {B}) /\ dom ( A X. {B}) = A))
13		dffunmo 3531	. . . . . 6 |- (Fun (A X. {B}) <-> (Rel (A X. {B}) /\ A.xE*y x(A X. {B})y))
14		relxp 3255	. . . . . 6 |- Rel (A X. {B})
15		moeq 1920	. . . . . . . . 9 |- E*y y = B
16	15	moani 1423	. . . . . . . 8 |- E*y(x e. A /\ y = B)
17		visset 1813	. . . . . . . . . . 11 |- y e. V
18	17	brxp 3215	. . . . . . . . . 10 |- (x(A X. {B})y <-> (x e. A /\ y e. {B}))
19		elsn 2421	. . . . . . . . . . 11 |- (y e. {B} <-> y = B)
20	19	anbi2i 480	. . . . . . . . . 10 |- ((x e. A /\ y e. {B}) <-> (x e. A /\ y = B))
21	18, 20	bitr 173	. . . . . . . . 9 |- (x(A X. {B})y <-> (x e. A /\ y = B))
22	21	mobii 1405	. . . . . . . 8 |- (E*y x(A X. {B})y <-> E*y(x e. A /\ y = B))
23	16, 22	mpbir 190	. . . . . . 7 |- E*y x(A X. {B})y
24	23	ax-gen 963	. . . . . 6 |- A.xE*y x(A X. {B})y
25	13, 14, 24	mpbir2an 730	. . . . 5 |- Fun (A X. {B})
26		fconst.1	. . . . . . 7 |- B e. V
27	26	snnz 2458	. . . . . 6 |- {B} =/= (/)
28		dmxp 3332	. . . . . 6 |- ({B} =/= (/) -> dom ( A X. {B}) = A)
29	27, 28	ax-mp 7	. . . . 5 |- dom ( A X. {B}) = A
30	12, 25, 29	mpbir2an 730	. . . 4 |- (A X. {B}) Fn A
31	11, 30	jctil 292	. . 3 |- (A =/= (/) -> ((A X. {B}) Fn A /\ ran ( A X. {B}) (_ {B}))
32		df-f 3194	. . 3 |- ((A X. {B}):A-->{B} <-> ((A X. {B}) Fn A /\ ran ( A X. {B}) (_ {B}))
33	31, 32	sylibr 200	. 2 |- (A =/= (/) -> (A X. {B}):A-->{B})
34	8, 33	pm2.61ine 1634	1 |- (A X. {B}):A-->{B}

Syntax hints:   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  E*wmo 1381   =/= wne 1585  Vcvv 1811   (_ wss 2047  (/)c0 2280  {csn 2409   class class class wbr 2619   X. cxp 3168  dom cdm 3170  ran crn 3171  Rel wrel 3175  Fun wfun 3176   Fn wfn 3177  -->wf 3178

This theorem is referenced by:  fconstg 3659  xpsn 3835  map0 4344  fodomr 4483  mapdom2lem 4493  mapdom2 4494  climuz0 7108  caucvg3t 7168  ser1clim0 7173  ser1cmp0 7175  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  acdc3lem 7486  acdclem 7494  ruclem39 7548  metelcls 7965  bcth 8032  0oo 8449  blocni 8465  ubthi 8544  hlim0 9105  ho01 9754  0cnfn 9904  0lnfn 9909

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620  df-opab 2667  df-id 2835  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-fun 3192  df-fn 3193  df-f 3194

Copyright terms: Public domain