Definition df-gch 9020

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 . A set satisfies the generalized continuum hypothesis if it is finite or there is no set strictly between and its powerset in cardinality. The continuum hypothesis is equivalent to . (Contributed by Mario Carneiro, 15-May-2015.)

Assertion

Ref	Expression
df-gch

Distinct variable group:   ,

Detailed syntax breakdown of Definition df-gch

Step	Hyp	Ref	Expression
1		cgch 9019	. 2
2		cfn 7536	. . 3
3		vx	. . . . . . . . 9
4	3	cv 1394	. . . . . . . 8
5		vy	. . . . . . . . 9
6	5	cv 1394	. . . . . . . 8
7		csdm 7535	. . . . . . . 8
8	4, 6, 7	wbr 4452	. . . . . . 7
9	4	cpw 4012	. . . . . . . 8
10	6, 9, 7	wbr 4452	. . . . . . 7
11	8, 10	wa 369	. . . . . 6
12	11	wn 3	. . . . 5
13	12, 5	wal 1393	. . . 4
14	13, 3	cab 2442	. . 3
15	2, 14	cun 3473	. 2
16	1, 15	wceq 1395	1

This definition is referenced by:  elgch  9021  fingch  9022