Theorem mapsnf1o

Description: A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypothesis	ixpsnf1o.f	$$⊢F=\left(x\in A⟼\left\{I\right\}\times \left\{x\right\}\right)$$
Assertion	mapsnf1o	$$⊢\left(A\in V\wedge I\in W\right)\to F:A\underset{1-1\; onto}{⟶}{A}^{\left\{I\right\}}$$

Proof

Step	Hyp	Ref	Expression
1		ixpsnf1o.f	$$⊢F=\left(x\in A⟼\left\{I\right\}\times \left\{x\right\}\right)$$
2	1	ixpsnf1o	$$⊢I\in W\to F:A\underset{1-1\; onto}{⟶}\underset{y\in \left\{I\right\}}{⨉}A$$
3	2	adantl	$$⊢\left(A\in V\wedge I\in W\right)\to F:A\underset{1-1\; onto}{⟶}\underset{y\in \left\{I\right\}}{⨉}A$$
4		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
5		ixpconstg	$$⊢\left(\left\{I\right\}\in \mathrm{V}\wedge A\in V\right)\to \underset{y\in \left\{I\right\}}{⨉}A=A^{\left\{I\right\}}$$
6	5	eqcomd	$$⊢\left(\left\{I\right\}\in \mathrm{V}\wedge A\in V\right)\to A^{\left\{I\right\}}=\underset{y\in \left\{I\right\}}{⨉}A$$
7	4 6	mpan	$$⊢A\in V\to A^{\left\{I\right\}}=\underset{y\in \left\{I\right\}}{⨉}A$$
8	7	adantr	$$⊢\left(A\in V\wedge I\in W\right)\to A^{\left\{I\right\}}=\underset{y\in \left\{I\right\}}{⨉}A$$
9	8	f1oeq3d	$$⊢\left(A\in V\wedge I\in W\right)\to \left(F:A\underset{1-1\; onto}{⟶}{A}^{\left\{I\right\}}\leftrightarrow F:A\underset{1-1\; onto}{⟶}\underset{y\in \left\{I\right\}}{⨉}A\right)$$
10	3 9	mpbird	$$⊢\left(A\in V\wedge I\in W\right)\to F:A\underset{1-1\; onto}{⟶}{A}^{\left\{I\right\}}$$