Theorem f1osng

Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013)

	Ref	Expression
Assertion	f1osng	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢a=A\to \left\{a\right\}=\left\{A\right\}$$
2	1	f1oeq2d	$$⊢a=A\to \left(\left\{⟨a,b⟩\right\}:\left\{a\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}\leftrightarrow \left\{⟨a,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}\right)$$
3		opeq1	$$⊢a=A\to ⟨a,b⟩=⟨A,b⟩$$
4	3	sneqd	$$⊢a=A\to \left\{⟨a,b⟩\right\}=\left\{⟨A,b⟩\right\}$$
5		f1oeq1	$$⊢\left\{⟨a,b⟩\right\}=\left\{⟨A,b⟩\right\}\to \left(\left\{⟨a,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}\leftrightarrow \left\{⟨A,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}\right)$$
6	4 5	syl	$$⊢a=A\to \left(\left\{⟨a,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}\leftrightarrow \left\{⟨A,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}\right)$$
7	2 6	bitrd	$$⊢a=A\to \left(\left\{⟨a,b⟩\right\}:\left\{a\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}\leftrightarrow \left\{⟨A,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}\right)$$
8		sneq	$$⊢b=B\to \left\{b\right\}=\left\{B\right\}$$
9	8	f1oeq3d	$$⊢b=B\to \left(\left\{⟨A,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}\leftrightarrow \left\{⟨A,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\right)$$
10		opeq2	$$⊢b=B\to ⟨A,b⟩=⟨A,B⟩$$
11	10	sneqd	$$⊢b=B\to \left\{⟨A,b⟩\right\}=\left\{⟨A,B⟩\right\}$$
12		f1oeq1	$$⊢\left\{⟨A,b⟩\right\}=\left\{⟨A,B⟩\right\}\to \left(\left\{⟨A,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\leftrightarrow \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\right)$$
13	11 12	syl	$$⊢b=B\to \left(\left\{⟨A,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\leftrightarrow \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\right)$$
14	9 13	bitrd	$$⊢b=B\to \left(\left\{⟨A,b⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}\leftrightarrow \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\right)$$
15		vex	$$⊢a\in \mathrm{V}$$
16		vex	$$⊢b\in \mathrm{V}$$
17	15 16	f1osn	$$⊢\left\{⟨a,b⟩\right\}:\left\{a\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}$$
18	7 14 17	vtocl2g	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$