Theorem wofi

Description: A total order on a finite set is a well-order. (Contributed by Jeff Madsen, 18-Jun-2010) (Proof shortened by Mario Carneiro, 29-Jan-2014)

	Ref	Expression
Assertion	wofi	$$⊢\left(R\mathrm{Or}A\wedge A\in \mathrm{Fin}\right)\to R\mathrm{We}A$$

Proof

Step	Hyp	Ref	Expression
1		sopo	$$⊢R\mathrm{Or}A\to R\mathrm{Po}A$$
2		frfi	$$⊢\left(R\mathrm{Po}A\wedge A\in \mathrm{Fin}\right)\to R\mathrm{Fr}A$$
3	1 2	sylan	$$⊢\left(R\mathrm{Or}A\wedge A\in \mathrm{Fin}\right)\to R\mathrm{Fr}A$$
4		simpl	$$⊢\left(R\mathrm{Or}A\wedge A\in \mathrm{Fin}\right)\to R\mathrm{Or}A$$
5		df-we	$$⊢R\mathrm{We}A\leftrightarrow \left(R\mathrm{Fr}A\wedge R\mathrm{Or}A\right)$$
6	3 4 5	sylanbrc	$$⊢\left(R\mathrm{Or}A\wedge A\in \mathrm{Fin}\right)\to R\mathrm{We}A$$