Theorem gch-kn

Description: The equivalence of two versions of the Generalized Continuum Hypothesis. The right-hand side is the standard version in the literature. The left-hand side is a version devised by Kannan Nambiar, which he calls the Axiom of Combinatorial Sets. For the notation and motivation behind this axiom, see his paper, "Derivation of Continuum Hypothesis from Axiom of Combinatorial Sets", available at http://www.e-atheneum.net/science/derivation_ch.pdf . The equivalence of the two sides provides a negative answer to Open Problem 2 in http://www.e-atheneum.net/science/open_problem_print.pdf . The key idea in the proof below is to equate both sides of alephexp2 to the successor aleph using enen2 . (Contributed by NM, 1-Oct-2004)

	Ref	Expression
Assertion	gch-kn	|- ( A e. On -> ( ( aleph ` suc A ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } <-> ( aleph ` suc A ) ~~ ( 2o ^m ( aleph ` A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		alephexp2	|- ( A e. On -> ( 2o ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } )
2		enen2	|- ( ( 2o ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } -> ( ( aleph ` suc A ) ~~ ( 2o ^m ( aleph ` A ) ) <-> ( aleph ` suc A ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } ) )
3	1 2	syl	|- ( A e. On -> ( ( aleph ` suc A ) ~~ ( 2o ^m ( aleph ` A ) ) <-> ( aleph ` suc A ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } ) )
4	3	bicomd	|- ( A e. On -> ( ( aleph ` suc A ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } <-> ( aleph ` suc A ) ~~ ( 2o ^m ( aleph ` A ) ) ) )