Theorem fconst 3643

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

Hypothesis

Ref	Expression
fconst.1	⊢ B ∈ V

Assertion

Ref	Expression
fconst	⊢ (A × {B}):A–→{B}

Proof of Theorem fconst

Step	Hyp	Ref	Expression
1		f0 3641	. . 3 ⊢ ∅:∅–→{B}
2		xpeq1 3190	. . . . . 6 ⊢ (A = ∅ → (A × {B}) = (∅ × {B}))
3		xp0r 3229	. . . . . 6 ⊢ (∅ × {B}) = ∅
4	2, 3	syl6eq 1515	. . . . 5 ⊢ (A = ∅ → (A × {B}) = ∅)
5	4	feq1d 3610	. . . 4 ⊢ (A = ∅ → ((A × {B}):A–→{B} ↔ ∅:A–→{B}))
6		feq2 3607	. . . 4 ⊢ (A = ∅ → (∅:A–→{B} ↔ ∅:∅–→{B}))
7	5, 6	bitrd 526	. . 3 ⊢ (A = ∅ → ((A × {B}):A–→{B} ↔ ∅:∅–→{B}))
8	1, 7	mpbiri 194	. 2 ⊢ (A = ∅ → (A × {B}):A–→{B})
9		rnxp 3458	. . . . 5 ⊢ (A ≠ ∅ → ran ( A × {B}) = {B})
10		eqimss 2099	. . . . 5 ⊢ (ran ( A × {B}) = {B} → ran ( A × {B}) ⊆ {B})
11	9, 10	syl 10	. . . 4 ⊢ (A ≠ ∅ → ran ( A × {B}) ⊆ {B})
12		df-fn 3183	. . . . 5 ⊢ ((A × {B}) Fn A ↔ (Fun (A × {B}) ⋀ dom ( A × {B}) = A))
13		dffunmo 3517	. . . . . 6 ⊢ (Fun (A × {B}) ↔ (Rel (A × {B}) ⋀ ∀x∃*y x(A × {B})y))
14		relxp 3245	. . . . . 6 ⊢ Rel (A × {B})
15		moeq 1911	. . . . . . . . 9 ⊢ ∃*y y = B
16	15	moani 1416	. . . . . . . 8 ⊢ ∃*y(x ∈ A ⋀ y = B)
17		visset 1804	. . . . . . . . . . 11 ⊢ y ∈ V
18	17	brxp 3205	. . . . . . . . . 10 ⊢ (x(A × {B})y ↔ (x ∈ A ⋀ y ∈ {B}))
19		elsn 2411	. . . . . . . . . . 11 ⊢ (y ∈ {B} ↔ y = B)
20	19	anbi2i 479	. . . . . . . . . 10 ⊢ ((x ∈ A ⋀ y ∈ {B}) ↔ (x ∈ A ⋀ y = B))
21	18, 20	bitr 173	. . . . . . . . 9 ⊢ (x(A × {B})y ↔ (x ∈ A ⋀ y = B))
22	21	mobii 1398	. . . . . . . 8 ⊢ (∃*y x(A × {B})y ↔ ∃*y(x ∈ A ⋀ y = B))
23	16, 22	mpbir 190	. . . . . . 7 ⊢ ∃*y x(A × {B})y
24	23	ax-gen 960	. . . . . 6 ⊢ ∀x∃*y x(A × {B})y
25	13, 14, 24	mpbir2an 728	. . . . 5 ⊢ Fun (A × {B})
26		fconst.1	. . . . . . 7 ⊢ B ∈ V
27	26	snnz 2449	. . . . . 6 ⊢ {B} ≠ ∅
28		dmxp 3321	. . . . . 6 ⊢ ({B} ≠ ∅ → dom ( A × {B}) = A)
29	27, 28	ax-mp 7	. . . . 5 ⊢ dom ( A × {B}) = A
30	12, 25, 29	mpbir2an 728	. . . 4 ⊢ (A × {B}) Fn A
31	11, 30	jctil 292	. . 3 ⊢ (A ≠ ∅ → ((A × {B}) Fn A ⋀ ran ( A × {B}) ⊆ {B}))
32		df-f 3184	. . 3 ⊢ ((A × {B}):A–→{B} ↔ ((A × {B}) Fn A ⋀ ran ( A × {B}) ⊆ {B}))
33	31, 32	sylibr 200	. 2 ⊢ (A ≠ ∅ → (A × {B}):A–→{B})
34	8, 33	pm2.61ine 1626	1 ⊢ (A × {B}):A–→{B}

Syntax hints:   ⋀ wa 223  ∀wal 951   = wceq 953   ∈ wcel 955  ∃*wmo 1374   ≠ wne 1577  Vcvv 1802   ⊆ wss 2037  ∅c0 2270  {csn 2399   class class class wbr 2609   × cxp 3158  dom cdm 3160  ran crn 3161  Rel wrel 3165  Fun wfun 3166   Fn wfn 3167  –→wf 3168

This theorem is referenced by:  fconstg 3644  xpsn 3820  map0 4328  fodomr 4463  mapdom2lem 4473  mapdom2 4474  climuz0 7045  caucvg3t 7104  ser1clim0 7109  ser1cmp0 7111  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  acdc3lem 7428  acdclem 7436  ruclem39 7491  metelcls 7900  bcth 7966  0oo 8381  blocni 8396  ubthi 8475  hlim0 9026  ho01 9671  0cnfn 9820  0lnfn 9825

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610  df-opab 2657  df-id 2824  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-fun 3182  df-fn 3183  df-f 3184

Copyright terms: Public domain