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