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 | |- ( ( R Or A /\ A e. Fin ) -> R We A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sopo | |- ( R Or A -> R Po A ) |
|
| 2 | frfi | |- ( ( R Po A /\ A e. Fin ) -> R Fr A ) |
|
| 3 | 1 2 | sylan | |- ( ( R Or A /\ A e. Fin ) -> R Fr A ) |
| 4 | simpl | |- ( ( R Or A /\ A e. Fin ) -> R Or A ) |
|
| 5 | df-we | |- ( R We A <-> ( R Fr A /\ R Or A ) ) |
|
| 6 | 3 4 5 | sylanbrc | |- ( ( R Or A /\ A e. Fin ) -> R We A ) |