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 )