Definition df-gch

Description: Define the collection of "GCH-sets", or sets for which the generalized continuum hypothesis holds. In this language the generalized continuum hypothesis can be expressed as GCH =V . A set x satisfies the generalized continuum hypothesis if it is finite or there is no set y strictly between x and its powerset in cardinality. The continuum hypothesis is equivalent to om e. GCH . (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	df-gch	|- GCH = ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgch	|- GCH
1		cfn	|- Fin
2		vx	|- x
3		vy	|- y
4	2	cv	|- x
5		csdm	|- ~<
6	3	cv	|- y
7	4 6 5	wbr	|- x ~< y
8	4	cpw	|- ~P x
9	6 8 5	wbr	|- y ~< ~P x
10	7 9	wa	|- ( x ~< y /\ y ~< ~P x )
11	10	wn	|- -. ( x ~< y /\ y ~< ~P x )
12	11 3	wal	|- A. y -. ( x ~< y /\ y ~< ~P x )
13	12 2	cab	|- { x | A. y -. ( x ~< y /\ y ~< ~P x ) }
14	1 13	cun	|- ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )
15	0 14	wceq	|- GCH = ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )