Theorem mapsnf1o2

Description: Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	mapsncnv.s	$$⊢S=\left\{X\right\}$$
	mapsncnv.b	$$⊢B\in \mathrm{V}$$
	mapsncnv.x	$$⊢X\in \mathrm{V}$$
	mapsncnv.f	$$⊢F=\left(x\in \left(B^S\right)⟼x\left(X\right)\right)$$
Assertion	mapsnf1o2	$$⊢F:B^S\underset{1-1\; onto}{⟶}B$$

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		mapsncnv.f	$$⊢F=\left(x\in \left(B^S\right)⟼x\left(X\right)\right)$$
5		fvex	$$⊢x\left(X\right)\in \mathrm{V}$$
6	5 4	fnmpti	$$⊢FFn\left(B^S\right)$$
7		snex	$$⊢\left\{X\right\}\in \mathrm{V}$$
8	1 7	eqeltri	$$⊢S\in \mathrm{V}$$
9		snex	$$⊢\left\{y\right\}\in \mathrm{V}$$
10	8 9	xpex	$$⊢S\times \left\{y\right\}\in \mathrm{V}$$
11	1 2 3 4	mapsncnv	$$⊢F^{-1}=\left(y\in B⟼S\times \left\{y\right\}\right)$$
12	10 11	fnmpti	$$⊢F^{-1}FnB$$
13		dff1o4	$$⊢F:B^S\underset{1-1\; onto}{⟶}B\leftrightarrow \left(FFn\left(B^S\right)\wedge F^{-1}FnB\right)$$
14	6 12 13	mpbir2an	$$⊢F:B^S\underset{1-1\; onto}{⟶}B$$