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∈V
2 omex ⊢ω∈V
3 1 2 unex ⊢x∪ω∈V
4 ssun2 ⊢ω⊆x∪ω
5 ssdomg ⊢x∪ω∈V→ω⊆x∪ω→ω≼x∪ω
6 3 4 5 mp2 ⊢ω≼x∪ω
7 id ⊢GCH=V→GCH=V
8 3 7 eleqtrrid ⊢GCH=V→x∪ω∈GCH
9 3 pwex ⊢𝒫x∪ω∈V
10 9 7 eleqtrrid ⊢GCH=V→𝒫x∪ω∈GCH
11 gchacg ⊢ω≼x∪ω∧x∪ω∈GCH∧𝒫x∪ω∈GCH→𝒫x∪ω∈dom⁡card
12 6 8 10 11 mp3an2i ⊢GCH=V→𝒫x∪ω∈dom⁡card
13 3 canth2 ⊢x∪ω≺𝒫x∪ω
14 sdomdom ⊢x∪ω≺𝒫x∪ω→x∪ω≼𝒫x∪ω
15 13 14 ax-mp ⊢x∪ω≼𝒫x∪ω
16 numdom ⊢𝒫x∪ω∈dom⁡card∧x∪ω≼𝒫x∪ω→x∪ω∈dom⁡card
17 12 15 16 sylancl ⊢GCH=V→x∪ω∈dom⁡card
18 ssun1 ⊢x⊆x∪ω
19 ssnum ⊢x∪ω∈dom⁡card∧x⊆x∪ω→x∈dom⁡card
20 17 18 19 sylancl ⊢GCH=V→x∈dom⁡card
21 1 a1i ⊢GCH=V→x∈V
22 20 21 2thd ⊢GCH=V→x∈dom⁡card↔x∈V
23 22 eqrdv ⊢GCH=V→dom⁡card=V
24 dfac10 ⊢CHOICE↔dom⁡card=V
25 23 24 sylibr ⊢GCH=V→CHOICE