Theorem elprchashprn2

Description: If one element of an unordered pair is not a set, the size of the unordered pair is not 2. (Contributed by Alexander van der Vekens, 7-Oct-2017)

	Ref	Expression
Assertion	elprchashprn2	$$⊢\neg M\in \mathrm{V}\to \neg \left|\left\{M,N\right\}\right|=2$$

Proof

Step	Hyp	Ref	Expression
1		prprc1	$$⊢\neg M\in \mathrm{V}\to \left\{M,N\right\}=\left\{N\right\}$$
2		hashsng	$$⊢N\in \mathrm{V}\to \left|\left\{N\right\}\right|=1$$
3		fveq2	$$⊢\left\{M,N\right\}=\left\{N\right\}\to \left|\left\{M,N\right\}\right|=\left|\left\{N\right\}\right|$$
4	3	eqcomd	$$⊢\left\{M,N\right\}=\left\{N\right\}\to \left|\left\{N\right\}\right|=\left|\left\{M,N\right\}\right|$$
5	4	eqeq1d	$$⊢\left\{M,N\right\}=\left\{N\right\}\to \left(\left|\left\{N\right\}\right|=1\leftrightarrow \left|\left\{M,N\right\}\right|=1\right)$$
6	5	biimpa	$$⊢\left(\left\{M,N\right\}=\left\{N\right\}\wedge \left|\left\{N\right\}\right|=1\right)\to \left|\left\{M,N\right\}\right|=1$$
7		id	$$⊢\left|\left\{M,N\right\}\right|=1\to \left|\left\{M,N\right\}\right|=1$$
8		1ne2	$$⊢1\ne 2$$
9	8	a1i	$$⊢\left|\left\{M,N\right\}\right|=1\to 1\ne 2$$
10	7 9	eqnetrd	$$⊢\left|\left\{M,N\right\}\right|=1\to \left|\left\{M,N\right\}\right|\ne 2$$
11	10	neneqd	$$⊢\left|\left\{M,N\right\}\right|=1\to \neg \left|\left\{M,N\right\}\right|=2$$
12	6 11	syl	$$⊢\left(\left\{M,N\right\}=\left\{N\right\}\wedge \left|\left\{N\right\}\right|=1\right)\to \neg \left|\left\{M,N\right\}\right|=2$$
13	12	expcom	$$⊢\left|\left\{N\right\}\right|=1\to \left(\left\{M,N\right\}=\left\{N\right\}\to \neg \left|\left\{M,N\right\}\right|=2\right)$$
14	2 13	syl	$$⊢N\in \mathrm{V}\to \left(\left\{M,N\right\}=\left\{N\right\}\to \neg \left|\left\{M,N\right\}\right|=2\right)$$
15		snprc	$$⊢\neg N\in \mathrm{V}\leftrightarrow \left\{N\right\}=\varnothing$$
16		eqeq2	$$⊢\left\{N\right\}=\varnothing \to \left(\left\{M,N\right\}=\left\{N\right\}\leftrightarrow \left\{M,N\right\}=\varnothing \right)$$
17	16	biimpa	$$⊢\left(\left\{N\right\}=\varnothing \wedge \left\{M,N\right\}=\left\{N\right\}\right)\to \left\{M,N\right\}=\varnothing$$
18		hash0	$$⊢\left|\varnothing \right|=0$$
19		fveq2	$$⊢\left\{M,N\right\}=\varnothing \to \left|\left\{M,N\right\}\right|=\left|\varnothing \right|$$
20	19	eqcomd	$$⊢\left\{M,N\right\}=\varnothing \to \left|\varnothing \right|=\left|\left\{M,N\right\}\right|$$
21	20	eqeq1d	$$⊢\left\{M,N\right\}=\varnothing \to \left(\left|\varnothing \right|=0\leftrightarrow \left|\left\{M,N\right\}\right|=0\right)$$
22	21	biimpa	$$⊢\left(\left\{M,N\right\}=\varnothing \wedge \left|\varnothing \right|=0\right)\to \left|\left\{M,N\right\}\right|=0$$
23		id	$$⊢\left|\left\{M,N\right\}\right|=0\to \left|\left\{M,N\right\}\right|=0$$
24		0ne2	$$⊢0\ne 2$$
25	24	a1i	$$⊢\left|\left\{M,N\right\}\right|=0\to 0\ne 2$$
26	23 25	eqnetrd	$$⊢\left|\left\{M,N\right\}\right|=0\to \left|\left\{M,N\right\}\right|\ne 2$$
27	26	neneqd	$$⊢\left|\left\{M,N\right\}\right|=0\to \neg \left|\left\{M,N\right\}\right|=2$$
28	22 27	syl	$$⊢\left(\left\{M,N\right\}=\varnothing \wedge \left|\varnothing \right|=0\right)\to \neg \left|\left\{M,N\right\}\right|=2$$
29	17 18 28	sylancl	$$⊢\left(\left\{N\right\}=\varnothing \wedge \left\{M,N\right\}=\left\{N\right\}\right)\to \neg \left|\left\{M,N\right\}\right|=2$$
30	29	ex	$$⊢\left\{N\right\}=\varnothing \to \left(\left\{M,N\right\}=\left\{N\right\}\to \neg \left|\left\{M,N\right\}\right|=2\right)$$
31	15 30	sylbi	$$⊢\neg N\in \mathrm{V}\to \left(\left\{M,N\right\}=\left\{N\right\}\to \neg \left|\left\{M,N\right\}\right|=2\right)$$
32	14 31	pm2.61i	$$⊢\left\{M,N\right\}=\left\{N\right\}\to \neg \left|\left\{M,N\right\}\right|=2$$
33	1 32	syl	$$⊢\neg M\in \mathrm{V}\to \neg \left|\left\{M,N\right\}\right|=2$$