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	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝑅 We 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		sopo	⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 )
2		frfi	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin ) → 𝑅 Fr 𝐴 )
3	1 2	sylan	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝑅 Fr 𝐴 )
4		simpl	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝑅 Or 𝐴 )
5		df-we	⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) )
6	3 4 5	sylanbrc	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝑅 We 𝐴 )