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	$$⊢\mathrm{GCH}=\mathrm{Fin}\cup \left\{x|\forall y\neg \left(x\prec y\wedge y\prec 𝒫x\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgch	$$class\mathrm{GCH}$$
1		cfn	$$class\mathrm{Fin}$$
2		vx	$$setvarx$$
3		vy	$$setvary$$
4	2	cv	$$setvarx$$
5		csdm	$$class\prec$$
6	3	cv	$$setvary$$
7	4 6 5	wbr	$$wffx\prec y$$
8	4	cpw	$$class𝒫x$$
9	6 8 5	wbr	$$wffy\prec 𝒫x$$
10	7 9	wa	$$wff\left(x\prec y\wedge y\prec 𝒫x\right)$$
11	10	wn	$$wff\neg \left(x\prec y\wedge y\prec 𝒫x\right)$$
12	11 3	wal	$$wff\forall y\neg \left(x\prec y\wedge y\prec 𝒫x\right)$$
13	12 2	cab	$$class\left\{x|\forall y\neg \left(x\prec y\wedge y\prec 𝒫x\right)\right\}$$
14	1 13	cun	$$class\left(\mathrm{Fin}\cup \left\{x|\forall y\neg \left(x\prec y\wedge y\prec 𝒫x\right)\right\}\right)$$
15	0 14	wceq	$$wff\mathrm{GCH}=\mathrm{Fin}\cup \left\{x|\forall y\neg \left(x\prec y\wedge y\prec 𝒫x\right)\right\}$$