Theorem f1o2sn

Description: A singleton consisting in a nested ordered pair is a one-to-one function from the cartesian product of two singletons onto a singleton (case where the two singletons are equal). (Contributed by AV, 15-Aug-2019)

	Ref	Expression
Assertion	f1o2sn	$$⊢\left(E\in V\wedge X\in W\right)\to \left\{⟨⟨E,E⟩,X⟩\right\}:\left\{E\right\}\times \left\{E\right\}\underset{1-1\; onto}{⟶}\left\{X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨E,E⟩\in \mathrm{V}$$
2		simpr	$$⊢\left(E\in V\wedge X\in W\right)\to X\in W$$
3		f1osng	$$⊢\left(⟨E,E⟩\in \mathrm{V}\wedge X\in W\right)\to \left\{⟨⟨E,E⟩,X⟩\right\}:\left\{⟨E,E⟩\right\}\underset{1-1\; onto}{⟶}\left\{X\right\}$$
4	1 2 3	sylancr	$$⊢\left(E\in V\wedge X\in W\right)\to \left\{⟨⟨E,E⟩,X⟩\right\}:\left\{⟨E,E⟩\right\}\underset{1-1\; onto}{⟶}\left\{X\right\}$$
5		xpsng	$$⊢\left(E\in V\wedge E\in V\right)\to \left\{E\right\}\times \left\{E\right\}=\left\{⟨E,E⟩\right\}$$
6	5	anidms	$$⊢E\in V\to \left\{E\right\}\times \left\{E\right\}=\left\{⟨E,E⟩\right\}$$
7	6	eqcomd	$$⊢E\in V\to \left\{⟨E,E⟩\right\}=\left\{E\right\}\times \left\{E\right\}$$
8	7	adantr	$$⊢\left(E\in V\wedge X\in W\right)\to \left\{⟨E,E⟩\right\}=\left\{E\right\}\times \left\{E\right\}$$
9	8	f1oeq2d	$$⊢\left(E\in V\wedge X\in W\right)\to \left(\left\{⟨⟨E,E⟩,X⟩\right\}:\left\{⟨E,E⟩\right\}\underset{1-1\; onto}{⟶}\left\{X\right\}\leftrightarrow \left\{⟨⟨E,E⟩,X⟩\right\}:\left\{E\right\}\times \left\{E\right\}\underset{1-1\; onto}{⟶}\left\{X\right\}\right)$$
10	4 9	mpbid	$$⊢\left(E\in V\wedge X\in W\right)\to \left\{⟨⟨E,E⟩,X⟩\right\}:\left\{E\right\}\times \left\{E\right\}\underset{1-1\; onto}{⟶}\left\{X\right\}$$