Theorem tpfi

Description: An unordered triple is finite. (Contributed by Mario Carneiro, 28-Sep-2013)

	Ref	Expression
Assertion	tpfi	$$⊢\left\{A,B,C\right\}\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		df-tp	$$⊢\left\{A,B,C\right\}=\left\{A,B\right\}\cup \left\{C\right\}$$
2		prfi	$$⊢\left\{A,B\right\}\in \mathrm{Fin}$$
3		snfi	$$⊢\left\{C\right\}\in \mathrm{Fin}$$
4		unfi	$$⊢\left(\left\{A,B\right\}\in \mathrm{Fin}\wedge \left\{C\right\}\in \mathrm{Fin}\right)\to \left\{A,B\right\}\cup \left\{C\right\}\in \mathrm{Fin}$$
5	2 3 4	mp2an	$$⊢\left\{A,B\right\}\cup \left\{C\right\}\in \mathrm{Fin}$$
6	1 5	eqeltri	$$⊢\left\{A,B,C\right\}\in \mathrm{Fin}$$