Description: The axiom of choice holds iff every aleph has a well-orderable powerset. (Contributed by Mario Carneiro, 21-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | dfac12 | |- ( CHOICE <-> A. x e. On ~P ( aleph ` x ) e. dom card ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfac12a | |- ( CHOICE <-> A. y e. On ~P y e. dom card ) |
|
2 | dfac12k | |- ( A. y e. On ~P y e. dom card <-> A. x e. On ~P ( aleph ` x ) e. dom card ) |
|
3 | 1 2 | bitri | |- ( CHOICE <-> A. x e. On ~P ( aleph ` x ) e. dom card ) |