Definition df-gch 8999

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 8998	. 2 class GCH
2		cfn 7515	. . 3 class Fin
3		vx	. . . . . . . . 9 setvar x
4	3	cv 1380	. . . . . . . 8 class x
5		vy	. . . . . . . . 9 setvar y
6	5	cv 1380	. . . . . . . 8 class y
7		csdm 7514	. . . . . . . 8 class ~<
8	4, 6, 7	wbr 4434	. . . . . . 7 wff x ~< y
9	4	cpw 3994	. . . . . . . 8 class ~P x
10	6, 9, 7	wbr 4434	. . . . . . 7 wff y ~< ~P x
11	8, 10	wa 369	. . . . . 6 wff ( x ~< y /\ y ~< ~P x )
12	11	wn 3	. . . . 5 wff -. ( x ~< y /\ y ~< ~P x )
13	12, 5	wal 1379	. . . 4 wff A. y -. ( x ~< y /\ y ~< ~P x )
14	13, 3	cab 2426	. . 3 class { x | A. y -. ( x ~< y /\ y ~< ~P x ) }
15	2, 14	cun 3457	. 2 class ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )
16	1, 15	wceq 1381	1 wff GCH = ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )

This definition is referenced by:  elgch  9000  fingch  9001