Theorem mapsnconst

Description: Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	mapsncnv.s	$$⊢S=\left\{X\right\}$$
	mapsncnv.b	$$⊢B\in \mathrm{V}$$
	mapsncnv.x	$$⊢X\in \mathrm{V}$$
Assertion	mapsnconst	$$⊢F\in \left(B^S\right)\to F=S\times \left\{F\left(X\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mapsncnv.s	$$⊢S=\left\{X\right\}$$
2		mapsncnv.b	$$⊢B\in \mathrm{V}$$
3		mapsncnv.x	$$⊢X\in \mathrm{V}$$
4		snex	$$⊢\left\{X\right\}\in \mathrm{V}$$
5	2 4	elmap	$$⊢F\in \left(B^{\left\{X\right\}}\right)\leftrightarrow F:\left\{X\right\}⟶B$$
6	3	fsn2	$$⊢F:\left\{X\right\}⟶B\leftrightarrow \left(F\left(X\right)\in B\wedge F=\left\{⟨X,F\left(X\right)⟩\right\}\right)$$
7	6	simprbi	$$⊢F:\left\{X\right\}⟶B\to F=\left\{⟨X,F\left(X\right)⟩\right\}$$
8	1	xpeq1i	$$⊢S\times \left\{F\left(X\right)\right\}=\left\{X\right\}\times \left\{F\left(X\right)\right\}$$
9		fvex	$$⊢F\left(X\right)\in \mathrm{V}$$
10	3 9	xpsn	$$⊢\left\{X\right\}\times \left\{F\left(X\right)\right\}=\left\{⟨X,F\left(X\right)⟩\right\}$$
11	8 10	eqtr2i	$$⊢\left\{⟨X,F\left(X\right)⟩\right\}=S\times \left\{F\left(X\right)\right\}$$
12	7 11	eqtrdi	$$⊢F:\left\{X\right\}⟶B\to F=S\times \left\{F\left(X\right)\right\}$$
13	5 12	sylbi	$$⊢F\in \left(B^{\left\{X\right\}}\right)\to F=S\times \left\{F\left(X\right)\right\}$$
14	1	oveq2i	$$⊢B^S=B^{\left\{X\right\}}$$
15	13 14	eleq2s	$$⊢F\in \left(B^S\right)\to F=S\times \left\{F\left(X\right)\right\}$$