Theorem en2

Description: A set equinumerous to ordinal 2 is an unordered pair. (Contributed by Mario Carneiro, 5-Jan-2016)

	Ref	Expression
Assertion	en2	$$⊢A\approx 2_{𝑜}\to \exists x\exists yA=\left\{x,y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
2	1	onordi	$$⊢\mathrm{Ord}{1}_{𝑜}$$
3		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
4		en1	$$⊢\left(A\setminus \left\{x\right\}\right)\approx 1_{𝑜}\leftrightarrow \exists yA\setminus \left\{x\right\}=\left\{y\right\}$$
5	4	biimpi	$$⊢\left(A\setminus \left\{x\right\}\right)\approx 1_{𝑜}\to \exists yA\setminus \left\{x\right\}=\left\{y\right\}$$
6		df-pr	$$⊢\left\{x,y\right\}=\left\{x\right\}\cup \left\{y\right\}$$
7	6	enp1ilem	$$⊢x\in A\to \left(A\setminus \left\{x\right\}=\left\{y\right\}\to A=\left\{x,y\right\}\right)$$
8	7	eximdv	$$⊢x\in A\to \left(\exists yA\setminus \left\{x\right\}=\left\{y\right\}\to \exists yA=\left\{x,y\right\}\right)$$
9	2 3 5 8	enp1i	$$⊢A\approx 2_{𝑜}\to \exists x\exists yA=\left\{x,y\right\}$$