Metamath Proof Explorer


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 𝐴 )