Theorem hash2pwpr

Description: If the size of a subset of an unordered pair is 2, the subset is the pair itself. (Contributed by Alexander van der Vekens, 9-Dec-2018)

	Ref	Expression
Assertion	hash2pwpr	$$⊢\left(\left|P\right|=2\wedge P\in 𝒫\left\{X,Y\right\}\right)\to P=\left\{X,Y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		pwpr	$$⊢𝒫\left\{X,Y\right\}=\left\{\varnothing ,\left\{X\right\}\right\}\cup \left\{\left\{Y\right\},\left\{X,Y\right\}\right\}$$
2	1	eleq2i	$$⊢P\in 𝒫\left\{X,Y\right\}\leftrightarrow P\in \left(\left\{\varnothing ,\left\{X\right\}\right\}\cup \left\{\left\{Y\right\},\left\{X,Y\right\}\right\}\right)$$
3		elun	$$⊢P\in \left(\left\{\varnothing ,\left\{X\right\}\right\}\cup \left\{\left\{Y\right\},\left\{X,Y\right\}\right\}\right)\leftrightarrow \left(P\in \left\{\varnothing ,\left\{X\right\}\right\}\vee P\in \left\{\left\{Y\right\},\left\{X,Y\right\}\right\}\right)$$
4	2 3	bitri	$$⊢P\in 𝒫\left\{X,Y\right\}\leftrightarrow \left(P\in \left\{\varnothing ,\left\{X\right\}\right\}\vee P\in \left\{\left\{Y\right\},\left\{X,Y\right\}\right\}\right)$$
5		fveq2	$$⊢P=\varnothing \to \left|P\right|=\left|\varnothing \right|$$
6		hash0	$$⊢\left|\varnothing \right|=0$$
7	6	eqeq2i	$$⊢\left|P\right|=\left|\varnothing \right|\leftrightarrow \left|P\right|=0$$
8		eqeq1	$$⊢\left|P\right|=0\to \left(\left|P\right|=2\leftrightarrow 0=2\right)$$
9		0ne2	$$⊢0\ne 2$$
10		eqneqall	$$⊢0=2\to \left(0\ne 2\to P=\left\{X,Y\right\}\right)$$
11	9 10	mpi	$$⊢0=2\to P=\left\{X,Y\right\}$$
12	8 11	biimtrdi	$$⊢\left|P\right|=0\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
13	7 12	sylbi	$$⊢\left|P\right|=\left|\varnothing \right|\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
14	5 13	syl	$$⊢P=\varnothing \to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
15		hashsng	$$⊢X\in \mathrm{V}\to \left|\left\{X\right\}\right|=1$$
16		fveq2	$$⊢\left\{X\right\}=P\to \left|\left\{X\right\}\right|=\left|P\right|$$
17	16	eqcoms	$$⊢P=\left\{X\right\}\to \left|\left\{X\right\}\right|=\left|P\right|$$
18	17	eqeq1d	$$⊢P=\left\{X\right\}\to \left(\left|\left\{X\right\}\right|=1\leftrightarrow \left|P\right|=1\right)$$
19		eqeq1	$$⊢\left|P\right|=1\to \left(\left|P\right|=2\leftrightarrow 1=2\right)$$
20		1ne2	$$⊢1\ne 2$$
21		eqneqall	$$⊢1=2\to \left(1\ne 2\to P=\left\{X,Y\right\}\right)$$
22	20 21	mpi	$$⊢1=2\to P=\left\{X,Y\right\}$$
23	19 22	biimtrdi	$$⊢\left|P\right|=1\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
24	18 23	biimtrdi	$$⊢P=\left\{X\right\}\to \left(\left|\left\{X\right\}\right|=1\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)\right)$$
25	15 24	syl5com	$$⊢X\in \mathrm{V}\to \left(P=\left\{X\right\}\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)\right)$$
26		snprc	$$⊢\neg X\in \mathrm{V}\leftrightarrow \left\{X\right\}=\varnothing$$
27		eqeq2	$$⊢\left\{X\right\}=\varnothing \to \left(P=\left\{X\right\}\leftrightarrow P=\varnothing \right)$$
28	5 6	eqtrdi	$$⊢P=\varnothing \to \left|P\right|=0$$
29	28	eqeq1d	$$⊢P=\varnothing \to \left(\left|P\right|=2\leftrightarrow 0=2\right)$$
30	29 11	biimtrdi	$$⊢P=\varnothing \to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
31	27 30	biimtrdi	$$⊢\left\{X\right\}=\varnothing \to \left(P=\left\{X\right\}\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)\right)$$
32	26 31	sylbi	$$⊢\neg X\in \mathrm{V}\to \left(P=\left\{X\right\}\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)\right)$$
33	25 32	pm2.61i	$$⊢P=\left\{X\right\}\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
34	14 33	jaoi	$$⊢\left(P=\varnothing \vee P=\left\{X\right\}\right)\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
35		hashsng	$$⊢Y\in \mathrm{V}\to \left|\left\{Y\right\}\right|=1$$
36		fveq2	$$⊢\left\{Y\right\}=P\to \left|\left\{Y\right\}\right|=\left|P\right|$$
37	36	eqcoms	$$⊢P=\left\{Y\right\}\to \left|\left\{Y\right\}\right|=\left|P\right|$$
38	37	eqeq1d	$$⊢P=\left\{Y\right\}\to \left(\left|\left\{Y\right\}\right|=1\leftrightarrow \left|P\right|=1\right)$$
39	38 23	biimtrdi	$$⊢P=\left\{Y\right\}\to \left(\left|\left\{Y\right\}\right|=1\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)\right)$$
40	35 39	syl5com	$$⊢Y\in \mathrm{V}\to \left(P=\left\{Y\right\}\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)\right)$$
41		snprc	$$⊢\neg Y\in \mathrm{V}\leftrightarrow \left\{Y\right\}=\varnothing$$
42		eqeq2	$$⊢\left\{Y\right\}=\varnothing \to \left(P=\left\{Y\right\}\leftrightarrow P=\varnothing \right)$$
43	5	eqeq1d	$$⊢P=\varnothing \to \left(\left|P\right|=2\leftrightarrow \left|\varnothing \right|=2\right)$$
44	6	eqeq1i	$$⊢\left|\varnothing \right|=2\leftrightarrow 0=2$$
45	44 11	sylbi	$$⊢\left|\varnothing \right|=2\to P=\left\{X,Y\right\}$$
46	43 45	biimtrdi	$$⊢P=\varnothing \to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
47	42 46	biimtrdi	$$⊢\left\{Y\right\}=\varnothing \to \left(P=\left\{Y\right\}\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)\right)$$
48	41 47	sylbi	$$⊢\neg Y\in \mathrm{V}\to \left(P=\left\{Y\right\}\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)\right)$$
49	40 48	pm2.61i	$$⊢P=\left\{Y\right\}\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
50		ax-1	$$⊢P=\left\{X,Y\right\}\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
51	49 50	jaoi	$$⊢\left(P=\left\{Y\right\}\vee P=\left\{X,Y\right\}\right)\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
52	34 51	jaoi	$$⊢\left(\left(P=\varnothing \vee P=\left\{X\right\}\right)\vee \left(P=\left\{Y\right\}\vee P=\left\{X,Y\right\}\right)\right)\to \left(\left|P\right|=2\to P=\left\{X,Y\right\}\right)$$
53		elpri	$$⊢P\in \left\{\varnothing ,\left\{X\right\}\right\}\to \left(P=\varnothing \vee P=\left\{X\right\}\right)$$
54		elpri	$$⊢P\in \left\{\left\{Y\right\},\left\{X,Y\right\}\right\}\to \left(P=\left\{Y\right\}\vee P=\left\{X,Y\right\}\right)$$
55	53 54	orim12i	$$⊢\left(P\in \left\{\varnothing ,\left\{X\right\}\right\}\vee P\in \left\{\left\{Y\right\},\left\{X,Y\right\}\right\}\right)\to \left(\left(P=\varnothing \vee P=\left\{X\right\}\right)\vee \left(P=\left\{Y\right\}\vee P=\left\{X,Y\right\}\right)\right)$$
56	52 55	syl11	$$⊢\left|P\right|=2\to \left(\left(P\in \left\{\varnothing ,\left\{X\right\}\right\}\vee P\in \left\{\left\{Y\right\},\left\{X,Y\right\}\right\}\right)\to P=\left\{X,Y\right\}\right)$$
57	4 56	biimtrid	$$⊢\left|P\right|=2\to \left(P\in 𝒫\left\{X,Y\right\}\to P=\left\{X,Y\right\}\right)$$
58	57	imp	$$⊢\left(\left|P\right|=2\wedge P\in 𝒫\left\{X,Y\right\}\right)\to P=\left\{X,Y\right\}$$