Theorem mapsnf1o3

Description: Explicit bijection in the reverse of mapsnf1o2 . (Contributed by Stefan O'Rear, 24-Mar-2015)

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

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		mapsnf1o3.f	$$⊢F=\left(y\in B⟼S\times \left\{y\right\}\right)$$
5		eqid	$$⊢\left(x\in \left(B^S\right)⟼x\left(X\right)\right)=\left(x\in \left(B^S\right)⟼x\left(X\right)\right)$$
6	1 2 3 5	mapsnf1o2	$$⊢\left(x\in \left(B^S\right)⟼x\left(X\right)\right):B^S\underset{1-1\; onto}{⟶}B$$
7		f1ocnv	$$⊢\left(x\in \left(B^S\right)⟼x\left(X\right)\right):B^S\underset{1-1\; onto}{⟶}B\to {\left(x\in \left(B^S\right)⟼x\left(X\right)\right)}^{-1}:B\underset{1-1\; onto}{⟶}{B}^S$$
8	6 7	ax-mp	$$⊢{\left(x\in \left(B^S\right)⟼x\left(X\right)\right)}^{-1}:B\underset{1-1\; onto}{⟶}{B}^S$$
9	1 2 3 5	mapsncnv	$$⊢{\left(x\in \left(B^S\right)⟼x\left(X\right)\right)}^{-1}=\left(y\in B⟼S\times \left\{y\right\}\right)$$
10	4 9	eqtr4i	$$⊢F={\left(x\in \left(B^S\right)⟼x\left(X\right)\right)}^{-1}$$
11		f1oeq1	$$⊢F={\left(x\in \left(B^S\right)⟼x\left(X\right)\right)}^{-1}\to \left(F:B\underset{1-1\; onto}{⟶}{B}^S\leftrightarrow {\left(x\in \left(B^S\right)⟼x\left(X\right)\right)}^{-1}:B\underset{1-1\; onto}{⟶}{B}^S\right)$$
12	10 11	ax-mp	$$⊢F:B\underset{1-1\; onto}{⟶}{B}^S\leftrightarrow {\left(x\in \left(B^S\right)⟼x\left(X\right)\right)}^{-1}:B\underset{1-1\; onto}{⟶}{B}^S$$
13	8 12	mpbir	$$⊢F:B\underset{1-1\; onto}{⟶}{B}^S$$