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