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 aleph C_ GCH )

Proof

Step Hyp Ref Expression
1 ssv 
 |-  ran aleph C_ _V
2 sseq2 
 |-  ( GCH = _V -> ( ran aleph C_ GCH <-> ran aleph C_ _V ) )
3 1 2 mpbiri 
 |-  ( GCH = _V -> ran aleph C_ GCH )
4 cardidm 
 |-  ( card ` ( card ` x ) ) = ( card ` x )
5 iscard3 
 |-  ( ( card ` ( card ` x ) ) = ( card ` x ) <-> ( card ` x ) e. ( _om u. ran aleph ) )
6 4 5 mpbi 
 |-  ( card ` x ) e. ( _om u. ran aleph )
7 elun 
 |-  ( ( card ` x ) e. ( _om u. ran aleph ) <-> ( ( card ` x ) e. _om \/ ( card ` x ) e. ran aleph ) )
8 6 7 mpbi 
 |-  ( ( card ` x ) e. _om \/ ( card ` x ) e. ran aleph )
9 fingch 
 |-  Fin C_ GCH
10 nnfi 
 |-  ( ( card ` x ) e. _om -> ( card ` x ) e. Fin )
11 9 10 sselid 
 |-  ( ( card ` x ) e. _om -> ( card ` x ) e. GCH )
12 11 a1i 
 |-  ( ran aleph C_ GCH -> ( ( card ` x ) e. _om -> ( card ` x ) e. GCH ) )
13 ssel 
 |-  ( ran aleph C_ GCH -> ( ( card ` x ) e. ran aleph -> ( card ` x ) e. GCH ) )
14 12 13 jaod 
 |-  ( ran aleph C_ GCH -> ( ( ( card ` x ) e. _om \/ ( card ` x ) e. ran aleph ) -> ( card ` x ) e. GCH ) )
15 8 14 mpi 
 |-  ( ran aleph C_ GCH -> ( card ` x ) e. GCH )
16 vex 
 |-  x e. _V
17 alephon 
 |-  ( aleph ` suc x ) e. On
18 simpr 
 |-  ( ( ran aleph C_ GCH /\ x e. On ) -> x e. On )
19 simpl 
 |-  ( ( ran aleph C_ GCH /\ x e. On ) -> ran aleph C_ GCH )
20 alephfnon 
 |-  aleph Fn On
21 fnfvelrn 
 |-  ( ( aleph Fn On /\ x e. On ) -> ( aleph ` x ) e. ran aleph )
22 20 18 21 sylancr 
 |-  ( ( ran aleph C_ GCH /\ x e. On ) -> ( aleph ` x ) e. ran aleph )
23 19 22 sseldd 
 |-  ( ( ran aleph C_ GCH /\ x e. On ) -> ( aleph ` x ) e. GCH )
24 onsuc 
 |-  ( x e. On -> suc x e. On )
25 24 adantl 
 |-  ( ( ran aleph C_ GCH /\ x e. On ) -> suc x e. On )
26 fnfvelrn 
 |-  ( ( aleph Fn On /\ suc x e. On ) -> ( aleph ` suc x ) e. ran aleph )
27 20 25 26 sylancr 
 |-  ( ( ran aleph C_ GCH /\ x e. On ) -> ( aleph ` suc x ) e. ran aleph )
28 19 27 sseldd 
 |-  ( ( ran aleph C_ GCH /\ x e. On ) -> ( aleph ` suc x ) e. GCH )
29 gchaleph2 
 |-  ( ( x e. On /\ ( aleph ` x ) e. GCH /\ ( aleph ` suc x ) e. GCH ) -> ( aleph ` suc x ) ~~ ~P ( aleph ` x ) )
30 18 23 28 29 syl3anc 
 |-  ( ( ran aleph C_ GCH /\ x e. On ) -> ( aleph ` suc x ) ~~ ~P ( aleph ` x ) )
31 isnumi 
 |-  ( ( ( aleph ` suc x ) e. On /\ ( aleph ` suc x ) ~~ ~P ( aleph ` x ) ) -> ~P ( aleph ` x ) e. dom card )
32 17 30 31 sylancr 
 |-  ( ( ran aleph C_ GCH /\ x e. On ) -> ~P ( aleph ` x ) e. dom card )
33 32 ralrimiva 
 |-  ( ran aleph C_ GCH -> A. x e. On ~P ( aleph ` x ) e. dom card )
34 dfac12 
 |-  ( CHOICE <-> A. x e. On ~P ( aleph ` x ) e. dom card )
35 33 34 sylibr 
 |-  ( ran aleph C_ GCH -> CHOICE )
36 dfac10 
 |-  ( CHOICE <-> dom card = _V )
37 35 36 sylib 
 |-  ( ran aleph C_ GCH -> dom card = _V )
38 16 37 eleqtrrid 
 |-  ( ran aleph C_ GCH -> x e. dom card )
39 cardid2 
 |-  ( x e. dom card -> ( card ` x ) ~~ x )
40 engch 
 |-  ( ( card ` x ) ~~ x -> ( ( card ` x ) e. GCH <-> x e. GCH ) )
41 38 39 40 3syl 
 |-  ( ran aleph C_ GCH -> ( ( card ` x ) e. GCH <-> x e. GCH ) )
42 15 41 mpbid 
 |-  ( ran aleph C_ GCH -> x e. GCH )
43 16 a1i 
 |-  ( ran aleph C_ GCH -> x e. _V )
44 42 43 2thd 
 |-  ( ran aleph C_ GCH -> ( x e. GCH <-> x e. _V ) )
45 44 eqrdv 
 |-  ( ran aleph C_ GCH -> GCH = _V )
46 3 45 impbii 
 |-  ( GCH = _V <-> ran aleph C_ GCH )