Theorem hash2pr

Description: A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017)

	Ref	Expression
Assertion	hash2pr	$$⊢\left(V\in W\wedge \left|V\right|=2\right)\to \exists a\exists bV=\left\{a,b\right\}$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		hashvnfin	$$⊢\left(V\in W\wedge 2\in {\mathbb{N}}_0\right)\to \left(\left|V\right|=2\to V\in \mathrm{Fin}\right)$$
3	1 2	mpan2	$$⊢V\in W\to \left(\left|V\right|=2\to V\in \mathrm{Fin}\right)$$
4	3	imp	$$⊢\left(V\in W\wedge \left|V\right|=2\right)\to V\in \mathrm{Fin}$$
5		hash2	$$⊢\left|2_{𝑜}\right|=2$$
6	5	eqcomi	$$⊢2=\left|2_{𝑜}\right|$$
7	6	a1i	$$⊢V\in \mathrm{Fin}\to 2=\left|2_{𝑜}\right|$$
8	7	eqeq2d	$$⊢V\in \mathrm{Fin}\to \left(\left|V\right|=2\leftrightarrow \left|V\right|=\left|2_{𝑜}\right|\right)$$
9		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
10		nnfi	$$⊢2_{𝑜}\in \mathrm{\omega }\to 2_{𝑜}\in \mathrm{Fin}$$
11	9 10	ax-mp	$$⊢2_{𝑜}\in \mathrm{Fin}$$
12		hashen	$$⊢\left(V\in \mathrm{Fin}\wedge 2_{𝑜}\in \mathrm{Fin}\right)\to \left(\left|V\right|=\left|2_{𝑜}\right|\leftrightarrow V\approx 2_{𝑜}\right)$$
13	11 12	mpan2	$$⊢V\in \mathrm{Fin}\to \left(\left|V\right|=\left|2_{𝑜}\right|\leftrightarrow V\approx 2_{𝑜}\right)$$
14	13	biimpd	$$⊢V\in \mathrm{Fin}\to \left(\left|V\right|=\left|2_{𝑜}\right|\to V\approx 2_{𝑜}\right)$$
15	8 14	sylbid	$$⊢V\in \mathrm{Fin}\to \left(\left|V\right|=2\to V\approx 2_{𝑜}\right)$$
16	15	adantld	$$⊢V\in \mathrm{Fin}\to \left(\left(V\in W\wedge \left|V\right|=2\right)\to V\approx 2_{𝑜}\right)$$
17	4 16	mpcom	$$⊢\left(V\in W\wedge \left|V\right|=2\right)\to V\approx 2_{𝑜}$$
18		en2	$$⊢V\approx 2_{𝑜}\to \exists a\exists bV=\left\{a,b\right\}$$
19	17 18	syl	$$⊢\left(V\in W\wedge \left|V\right|=2\right)\to \exists a\exists bV=\left\{a,b\right\}$$