Theorem hashtplei

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

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

Proof

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