Theorem fconst 3733

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 3731	. . 3 |- (/):(/)-->{B}
2		xpeq1 3255	. . . . . 6 |- (A = (/) -> (A X. {B}) = ((/) X. {B}))
3		xp0r 3298	. . . . . 6 |- ((/) X. {B}) = (/)
4	2, 3	syl6eq 1560	. . . . 5 |- (A = (/) -> (A X. {B}) = (/))
5	4	feq1d 3699	. . . 4 |- (A = (/) -> ((A X. {B}):A-->{B} <-> (/):A-->{B}))
6		feq2 3696	. . . 4 |- (A = (/) -> ((/):A-->{B} <-> (/):(/)-->{B}))
7	5, 6	bitrd 530	. . 3 |- (A = (/) -> ((A X. {B}):A-->{B} <-> (/):(/)-->{B}))
8	1, 7	mpbiri 192	. 2 |- (A = (/) -> (A X. {B}):A-->{B})
9		rnxp 3528	. . . . 5 |- (A =/= (/) -> ran ( A X. {B}) = {B})
10		eqimss 2153	. . . . 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 3248	. . . . 5 |- ((A X. {B}) Fn A <-> (Fun (A X. {B}) /\ dom ( A X. {B}) = A))
13		dffun6 3606	. . . . . 6 |- (Fun (A X. {B}) <-> (Rel (A X. {B}) /\ A.xE*y x(A X. {B})y))
14		relxp 3317	. . . . . 6 |- Rel (A X. {B})
15		moeq 1958	. . . . . . . . 9 |- E*y y = B
16	15	moani 1456	. . . . . . . 8 |- E*y(x e. A /\ y = B)
17		visset 1851	. . . . . . . . . . 11 |- y e. V
18	17	brxp 3272	. . . . . . . . . 10 |- (x(A X. {B})y <-> (x e. A /\ y e. {B}))
19		elsn 2466	. . . . . . . . . . 11 |- (y e. {B} <-> y = B)
20	19	anbi2i 482	. . . . . . . . . 10 |- ((x e. A /\ y e. {B}) <-> (x e. A /\ y = B))
21	18, 20	bitri 171	. . . . . . . . 9 |- (x(A X. {B})y <-> (x e. A /\ y = B))
22	21	mobii 1438	. . . . . . . 8 |- (E*y x(A X. {B})y <-> E*y(x e. A /\ y = B))
23	16, 22	mpbir 188	. . . . . . 7 |- E*y x(A X. {B})y
24	23	ax-gen 995	. . . . . 6 |- A.xE*y x(A X. {B})y
25	13, 14, 24	mpbir2an 733	. . . . 5 |- Fun (A X. {B})
26		fconst.1	. . . . . . 7 |- B e. V
27	26	snnz 2506	. . . . . 6 |- {B} =/= (/)
28		dmxp 3392	. . . . . 6 |- ({B} =/= (/) -> dom ( A X. {B}) = A)
29	27, 28	ax-mp 7	. . . . 5 |- dom ( A X. {B}) = A
30	12, 25, 29	mpbir2an 733	. . . 4 |- (A X. {B}) Fn A
31	11, 30	jctil 290	. . 3 |- (A =/= (/) -> ((A X. {B}) Fn A /\ ran ( A X. {B}) (_ {B}))
32		df-f 3249	. . 3 |- ((A X. {B}):A-->{B} <-> ((A X. {B}) Fn A /\ ran ( A X. {B}) (_ {B}))
33	31, 32	sylibr 198	. 2 |- (A =/= (/) -> (A X. {B}):A-->{B})
34	8, 33	pm2.61ine 1672	1 |- (A X. {B}):A-->{B}

Syntax hints:   /\ wa 221  A.wal 986   = wceq 988   e. wcel 990  E*wmo 1414   =/= wne 1622  Vcvv 1849   (_ wss 2091  (/)c0 2324  {csn 2454   class class class wbr 2669   X. cxp 3223  dom cdm 3225  ran crn 3226  Rel wrel 3230  Fun wfun 3231   Fn wfn 3232  -->wf 3233

This theorem is referenced by:  fconstg 3734  xpsn 3911  map0 4431  fodomr 4570  mapdom2lem 4582  mapdom2 4583  climuz0i 7231  caucvg3 7291  ser1clim0 7296  ser1cmp0i 7298  cvgcmp3cetlem1 7311  cvgcmp3cetlem2 7312  acdc3lem 7611  acdclem 7619  ruclem39 7673  metelcls 8085  bcth 8152  0oo 8568  blocni 8584  ubthi 8663  hlim0 9225  ho01i 9874  0cnfn 10021  0lnfn 10026

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-9 997  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-nul 2761  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-rel 3240  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-fun 3247  df-fn 3248  df-f 3249

Copyright terms: Public domain