Theorem hashprdifel

Description: The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020)

	Ref	Expression
Hypothesis	hashprdifel.s	$$⊢S=\left\{A,B\right\}$$
Assertion	hashprdifel	$$⊢\left|S\right|=2\to \left(A\in S\wedge B\in S\wedge A\ne B\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashprdifel.s	$$⊢S=\left\{A,B\right\}$$
2	1	fveq2i	$$⊢\left|S\right|=\left|\left\{A,B\right\}\right|$$
3	2	eqeq1i	$$⊢\left|S\right|=2\leftrightarrow \left|\left\{A,B\right\}\right|=2$$
4		hashprb	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\leftrightarrow \left|\left\{A,B\right\}\right|=2$$
5	3 4	bitr4i	$$⊢\left|S\right|=2\leftrightarrow \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)$$
6		prid1g	$$⊢A\in \mathrm{V}\to A\in \left\{A,B\right\}$$
7	6	3ad2ant1	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to A\in \left\{A,B\right\}$$
8	7 1	eleqtrrdi	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to A\in S$$
9		prid2g	$$⊢B\in \mathrm{V}\to B\in \left\{A,B\right\}$$
10	9	3ad2ant2	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to B\in \left\{A,B\right\}$$
11	10 1	eleqtrrdi	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to B\in S$$
12		simp3	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to A\ne B$$
13	8 11 12	3jca	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge A\ne B\right)\to \left(A\in S\wedge B\in S\wedge A\ne B\right)$$
14	5 13	sylbi	$$⊢\left|S\right|=2\to \left(A\in S\wedge B\in S\wedge A\ne B\right)$$