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	4	f1oeq1d	$$⊢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)$$
6	2 5	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)$$
7		sneq	$$⊢b=B\to \left\{b\right\}=\left\{B\right\}$$
8	7	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)$$
9		opeq2	$$⊢b=B\to ⟨A,b⟩=⟨A,B⟩$$
10	9	sneqd	$$⊢b=B\to \left\{⟨A,b⟩\right\}=\left\{⟨A,B⟩\right\}$$
11	10	f1oeq1d	$$⊢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)$$
12	8 11	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)$$
13		vex	$$⊢a\in \mathrm{V}$$
14		vex	$$⊢b\in \mathrm{V}$$
15	13 14	f1osn	$$⊢\left\{⟨a,b⟩\right\}:\left\{a\right\}\underset{1-1\; onto}{⟶}\left\{b\right\}$$
16	6 12 15	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\}$$