Theorem hashprlei

Description: An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	hashprlei	$$⊢\left(\left\{A,B\right\}\in \mathrm{Fin}\wedge \left|\left\{A,B\right\}\right|\le 2\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
2		hashsnlei	$$⊢\left(\left\{A\right\}\in \mathrm{Fin}\wedge \left|\left\{A\right\}\right|\le 1\right)$$
3		hashsnlei	$$⊢\left(\left\{B\right\}\in \mathrm{Fin}\wedge \left|\left\{B\right\}\right|\le 1\right)$$
4		1nn0	$$⊢1\in {\mathbb{N}}_0$$
5		1p1e2	$$⊢1+1=2$$
6	1 2 3 4 4 5	hashunlei	$$⊢\left(\left\{A,B\right\}\in \mathrm{Fin}\wedge \left|\left\{A,B\right\}\right|\le 2\right)$$