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

Metamath Proof Explorer

Theorem gch2

Description: It is sufficient to require that all alephs are GCH-sets to ensure the full generalized continuum hypothesis. (The proof uses the Axiom of Regularity.) (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion gch2 ( GCH = V ↔ ran ℵ ⊆ GCH )

Proof

Step Hyp Ref Expression
1 ssv ⊢ ran ℵ ⊆ V
2 sseq2 ⊢ ( GCH = V → ( ran ℵ ⊆ GCH ↔ ran ℵ ⊆ V ) )
3 1 2 mpbiri ⊢ ( GCH = V → ran ℵ ⊆ GCH )
4 cardidm ⊢ ( card ‘ ( card ‘ 𝑥 ) ) = ( card ‘ 𝑥 )
5 iscard3 ⊢ ( ( card ‘ ( card ‘ 𝑥 ) ) = ( card ‘ 𝑥 ) ↔ ( card ‘ 𝑥 ) ∈ ( ω ∪ ran ℵ ) )
6 4 5 mpbi ⊢ ( card ‘ 𝑥 ) ∈ ( ω ∪ ran ℵ )
7 elun ⊢ ( ( card ‘ 𝑥 ) ∈ ( ω ∪ ran ℵ ) ↔ ( ( card ‘ 𝑥 ) ∈ ω ∨ ( card ‘ 𝑥 ) ∈ ran ℵ ) )
8 6 7 mpbi ⊢ ( ( card ‘ 𝑥 ) ∈ ω ∨ ( card ‘ 𝑥 ) ∈ ran ℵ )
9 fingch ⊢ Fin ⊆ GCH
10 nnfi ⊢ ( ( card ‘ 𝑥 ) ∈ ω → ( card ‘ 𝑥 ) ∈ Fin )
11 9 10 sselid ⊢ ( ( card ‘ 𝑥 ) ∈ ω → ( card ‘ 𝑥 ) ∈ GCH )
12 11 a1i ⊢ ( ran ℵ ⊆ GCH → ( ( card ‘ 𝑥 ) ∈ ω → ( card ‘ 𝑥 ) ∈ GCH ) )
13 ssel ⊢ ( ran ℵ ⊆ GCH → ( ( card ‘ 𝑥 ) ∈ ran ℵ → ( card ‘ 𝑥 ) ∈ GCH ) )
14 12 13 jaod ⊢ ( ran ℵ ⊆ GCH → ( ( ( card ‘ 𝑥 ) ∈ ω ∨ ( card ‘ 𝑥 ) ∈ ran ℵ ) → ( card ‘ 𝑥 ) ∈ GCH ) )
15 8 14 mpi ⊢ ( ran ℵ ⊆ GCH → ( card ‘ 𝑥 ) ∈ GCH )
16 vex ⊢ 𝑥 ∈ V
17 alephon ⊢ ( ℵ ‘ suc 𝑥 ) ∈ On
18 simpr ⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → 𝑥 ∈ On )
19 simpl ⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ran ℵ ⊆ GCH )
20 alephfnon ⊢ ℵ Fn On
21 fnfvelrn ⊢ ( ( ℵ Fn On ∧ 𝑥 ∈ On ) → ( ℵ ‘ 𝑥 ) ∈ ran ℵ )
22 20 18 21 sylancr ⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ( ℵ ‘ 𝑥 ) ∈ ran ℵ )
23 19 22 sseldd ⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ( ℵ ‘ 𝑥 ) ∈ GCH )
24 onsuc ⊢ ( 𝑥 ∈ On → suc 𝑥 ∈ On )
25 24 adantl ⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → suc 𝑥 ∈ On )
26 fnfvelrn ⊢ ( ( ℵ Fn On ∧ suc 𝑥 ∈ On ) → ( ℵ ‘ suc 𝑥 ) ∈ ran ℵ )
27 20 25 26 sylancr ⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ( ℵ ‘ suc 𝑥 ) ∈ ran ℵ )
28 19 27 sseldd ⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ( ℵ ‘ suc 𝑥 ) ∈ GCH )
29 gchaleph2 ⊢ ( ( 𝑥 ∈ On ∧ ( ℵ ‘ 𝑥 ) ∈ GCH ∧ ( ℵ ‘ suc 𝑥 ) ∈ GCH ) → ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) )
30 18 23 28 29 syl3anc ⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) )
31 isnumi ⊢ ( ( ( ℵ ‘ suc 𝑥 ) ∈ On ∧ ( ℵ ‘ suc 𝑥 ) ≈ 𝒫 ( ℵ ‘ 𝑥 ) ) → 𝒫 ( ℵ ‘ 𝑥 ) ∈ dom card )
32 17 30 31 sylancr ⊢ ( ( ran ℵ ⊆ GCH ∧ 𝑥 ∈ On ) → 𝒫 ( ℵ ‘ 𝑥 ) ∈ dom card )
33 32 ralrimiva ⊢ ( ran ℵ ⊆ GCH → ∀ 𝑥 ∈ On 𝒫 ( ℵ ‘ 𝑥 ) ∈ dom card )
34 dfac12 ⊢ ( CHOICE ↔ ∀ 𝑥 ∈ On 𝒫 ( ℵ ‘ 𝑥 ) ∈ dom card )
35 33 34 sylibr ⊢ ( ran ℵ ⊆ GCH → CHOICE )
36 dfac10 ⊢ ( CHOICE ↔ dom card = V )
37 35 36 sylib ⊢ ( ran ℵ ⊆ GCH → dom card = V )
38 16 37 eleqtrrid ⊢ ( ran ℵ ⊆ GCH → 𝑥 ∈ dom card )
39 cardid2 ⊢ ( 𝑥 ∈ dom card → ( card ‘ 𝑥 ) ≈ 𝑥 )
40 engch ⊢ ( ( card ‘ 𝑥 ) ≈ 𝑥 → ( ( card ‘ 𝑥 ) ∈ GCH ↔ 𝑥 ∈ GCH ) )
41 38 39 40 3syl ⊢ ( ran ℵ ⊆ GCH → ( ( card ‘ 𝑥 ) ∈ GCH ↔ 𝑥 ∈ GCH ) )
42 15 41 mpbid ⊢ ( ran ℵ ⊆ GCH → 𝑥 ∈ GCH )
43 16 a1i ⊢ ( ran ℵ ⊆ GCH → 𝑥 ∈ V )
44 42 43 2thd ⊢ ( ran ℵ ⊆ GCH → ( 𝑥 ∈ GCH ↔ 𝑥 ∈ V ) )
45 44 eqrdv ⊢ ( ran ℵ ⊆ GCH → GCH = V )
46 3 45 impbii ⊢ ( GCH = V ↔ ran ℵ ⊆ GCH )