Metamath Proof Explorer

Theorem dfac12

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 )

Proof

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 )