Metamath Proof Explorer

Theorem gchac

Description: The Generalized Continuum Hypothesis implies the Axiom of Choice. The original proof is due to Sierpiński (1947); we use a refinement of Sierpiński's result due to Specker. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion gchac 
|- ( GCH = _V -> CHOICE )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 omex 
 |-  _om e. _V
3 1 2 unex 
 |-  ( x u. _om ) e. _V
4 ssun2 
 |-  _om C_ ( x u. _om )
5 ssdomg 
 |-  ( ( x u. _om ) e. _V -> ( _om C_ ( x u. _om ) -> _om ~<_ ( x u. _om ) ) )
6 3 4 5 mp2 
 |-  _om ~<_ ( x u. _om )
7 id 
 |-  ( GCH = _V -> GCH = _V )
8 3 7 eleqtrrid 
 |-  ( GCH = _V -> ( x u. _om ) e. GCH )
9 3 pwex 
 |-  ~P ( x u. _om ) e. _V
10 9 7 eleqtrrid 
 |-  ( GCH = _V -> ~P ( x u. _om ) e. GCH )
11 gchacg 
 |-  ( ( _om ~<_ ( x u. _om ) /\ ( x u. _om ) e. GCH /\ ~P ( x u. _om ) e. GCH ) -> ~P ( x u. _om ) e. dom card )
12 6 8 10 11 mp3an2i 
 |-  ( GCH = _V -> ~P ( x u. _om ) e. dom card )
13 3 canth2 
 |-  ( x u. _om ) ~< ~P ( x u. _om )
14 sdomdom 
 |-  ( ( x u. _om ) ~< ~P ( x u. _om ) -> ( x u. _om ) ~<_ ~P ( x u. _om ) )
15 13 14 ax-mp 
 |-  ( x u. _om ) ~<_ ~P ( x u. _om )
16 numdom 
 |-  ( ( ~P ( x u. _om ) e. dom card /\ ( x u. _om ) ~<_ ~P ( x u. _om ) ) -> ( x u. _om ) e. dom card )
17 12 15 16 sylancl 
 |-  ( GCH = _V -> ( x u. _om ) e. dom card )
18 ssun1 
 |-  x C_ ( x u. _om )
19 ssnum 
 |-  ( ( ( x u. _om ) e. dom card /\ x C_ ( x u. _om ) ) -> x e. dom card )
20 17 18 19 sylancl 
 |-  ( GCH = _V -> x e. dom card )
21 1 a1i 
 |-  ( GCH = _V -> x e. _V )
22 20 21 2thd 
 |-  ( GCH = _V -> ( x e. dom card <-> x e. _V ) )
23 22 eqrdv 
 |-  ( GCH = _V -> dom card = _V )
24 dfac10 
 |-  ( CHOICE <-> dom card = _V )
25 23 24 sylibr 
 |-  ( GCH = _V -> CHOICE )