Definition df-gch 9322

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 𝑥 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 ω ∈ GCH. (Contributed by Mario Carneiro, 15-May-2015.)

Assertion

Ref	Expression
df-gch	⊢ GCH = (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)})

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-gch

Step	Hyp	Ref	Expression
1		cgch 9321	. 2 class GCH
2		cfn 7841	. . 3 class Fin
3		vx	. . . . . . . . 9 setvar 𝑥
4	3	cv 1474	. . . . . . . 8 class 𝑥
5		vy	. . . . . . . . 9 setvar 𝑦
6	5	cv 1474	. . . . . . . 8 class 𝑦
7		csdm 7840	. . . . . . . 8 class ≺
8	4, 6, 7	wbr 4583	. . . . . . 7 wff 𝑥 ≺ 𝑦
9	4	cpw 4108	. . . . . . . 8 class 𝒫 𝑥
10	6, 9, 7	wbr 4583	. . . . . . 7 wff 𝑦 ≺ 𝒫 𝑥
11	8, 10	wa 383	. . . . . 6 wff (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)
12	11	wn 3	. . . . 5 wff ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)
13	12, 5	wal 1473	. . . 4 wff ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)
14	13, 3	cab 2596	. . 3 class {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)}
15	2, 14	cun 3538	. 2 class (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)})
16	1, 15	wceq 1475	1 wff GCH = (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)})

This definition is referenced by:  elgch  9323  fingch  9324