This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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