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