Metamath Proof Explorer

Theorem dfac12a

Description: The axiom of choice holds iff every ordinal has a well-orderable powerset. (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion dfac12a 
|- ( CHOICE <-> A. x e. On ~P x e. dom card )

Proof

Step Hyp Ref Expression
1 ssv 
 |-  dom card C_ _V
2 eqss 
 |-  ( dom card = _V <-> ( dom card C_ _V /\ _V C_ dom card ) )
3 1 2 mpbiran 
 |-  ( dom card = _V <-> _V C_ dom card )
4 dfac10 
 |-  ( CHOICE <-> dom card = _V )
5 unir1 
 |-  U. ( R1 " On ) = _V
6 5 sseq1i 
 |-  ( U. ( R1 " On ) C_ dom card <-> _V C_ dom card )
7 3 4 6 3bitr4i 
 |-  ( CHOICE <-> U. ( R1 " On ) C_ dom card )
8 dfac12r 
 |-  ( A. x e. On ~P x e. dom card <-> U. ( R1 " On ) C_ dom card )
9 7 8 bitr4i 
 |-  ( CHOICE <-> A. x e. On ~P x e. dom card )