Theorem f1sng

Description: A singleton of an ordered pair is a one-to-one function. (Contributed by AV, 17-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		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\}$$
2		f1of1	$$⊢\left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\to \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}\left\{B\right\}$$
3	1 2	syl	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}\left\{B\right\}$$
4		snssi	$$⊢B\in W\to \left\{B\right\}\subseteq W$$
5	4	adantl	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{B\right\}\subseteq W$$
6		f1ss	$$⊢\left(\left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}\left\{B\right\}\wedge \left\{B\right\}\subseteq W\right)\to \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}W$$
7	3 5 6	syl2anc	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{⟨A,B⟩\right\}:\left\{A\right\}\underset{1-1}{⟶}W$$