Definition df-gch 9443

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.)

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-gch

Step	Hyp	Ref	Expression
1		cgch 9442	. 2 class GCH
2		cfn 7955	. . 3 class Fin
3		vx	. . . . . . . . 9 setvar x
4	3	cv 1482	. . . . . . . 8 class x
5		vy	. . . . . . . . 9 setvar y
6	5	cv 1482	. . . . . . . 8 class y
7		csdm 7954	. . . . . . . 8 class ~<
8	4, 6, 7	wbr 4653	. . . . . . 7 wff x ~< y
9	4	cpw 4158	. . . . . . . 8 class ~P x
10	6, 9, 7	wbr 4653	. . . . . . 7 wff y ~< ~P x
11	8, 10	wa 384	. . . . . 6 wff ( x ~< y /\ y ~< ~P x )
12	11	wn 3	. . . . 5 wff -. ( x ~< y /\ y ~< ~P x )
13	12, 5	wal 1481	. . . 4 wff A. y -. ( x ~< y /\ y ~< ~P x )
14	13, 3	cab 2608	. . 3 class { x | A. y -. ( x ~< y /\ y ~< ~P x ) }
15	2, 14	cun 3572	. 2 class ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )
16	1, 15	wceq 1483	1 wff GCH = ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )

This definition is referenced by:  elgch  9444  fingch  9445