Theorem f1osn

Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by NM, 18-May-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Hypotheses	f1osn.1	$$⊢A\in \mathrm{V}$$
	f1osn.2	$$⊢B\in \mathrm{V}$$
Assertion	f1osn	$$⊢\left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		f1osn.1	$$⊢A\in \mathrm{V}$$
2		f1osn.2	$$⊢B\in \mathrm{V}$$
3	1 2	fnsn	$$⊢\left\{⟨A,B⟩\right\}Fn\left\{A\right\}$$
4	2 1	fnsn	$$⊢\left\{⟨B,A⟩\right\}Fn\left\{B\right\}$$
5	1 2	cnvsn	$$⊢{\left\{⟨A,B⟩\right\}}^{-1}=\left\{⟨B,A⟩\right\}$$
6	5	fneq1i	$$⊢{\left\{⟨A,B⟩\right\}}^{-1}Fn\left\{B\right\}\leftrightarrow \left\{⟨B,A⟩\right\}Fn\left\{B\right\}$$
7	4 6	mpbir	$$⊢{\left\{⟨A,B⟩\right\}}^{-1}Fn\left\{B\right\}$$
8		dff1o4	$$⊢\left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\leftrightarrow \left(\left\{⟨A,B⟩\right\}Fn\left\{A\right\}\wedge {\left\{⟨A,B⟩\right\}}^{-1}Fn\left\{B\right\}\right)$$
9	3 7 8	mpbir2an	$$⊢\left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$