Description: Well-ordering theorem: any set A can be well-ordered. This is an equivalent of the Axiom of Choice. Theorem 6 of Suppes p. 242. First proved by Ernst Zermelo (the "Z" in ZFC) in 1904. (Contributed by Mario Carneiro, 5-Jan-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | weth | |- ( A e. V -> E. x x We A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | weeq2 | |- ( y = A -> ( x We y <-> x We A ) ) |
|
| 2 | 1 | exbidv | |- ( y = A -> ( E. x x We y <-> E. x x We A ) ) |
| 3 | dfac8 | |- ( CHOICE <-> A. y E. x x We y ) |
|
| 4 | 3 | axaci | |- E. x x We y |
| 5 | 2 4 | vtoclg | |- ( A e. V -> E. x x We A ) |