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