MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gch Structured version   Visualization version   GIF version

Definition df-gch 9440
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
StepHypRef Expression
1 cgch 9439 . 2 class GCH
2 cfn 7952 . . 3 class Fin
3 vx . . . . . . . . 9 setvar 𝑥
43cv 1481 . . . . . . . 8 class 𝑥
5 vy . . . . . . . . 9 setvar 𝑦
65cv 1481 . . . . . . . 8 class 𝑦
7 csdm 7951 . . . . . . . 8 class
84, 6, 7wbr 4651 . . . . . . 7 wff 𝑥𝑦
94cpw 4156 . . . . . . . 8 class 𝒫 𝑥
106, 9, 7wbr 4651 . . . . . . 7 wff 𝑦 ≺ 𝒫 𝑥
118, 10wa 384 . . . . . 6 wff (𝑥𝑦𝑦 ≺ 𝒫 𝑥)
1211wn 3 . . . . 5 wff ¬ (𝑥𝑦𝑦 ≺ 𝒫 𝑥)
1312, 5wal 1480 . . . 4 wff 𝑦 ¬ (𝑥𝑦𝑦 ≺ 𝒫 𝑥)
1413, 3cab 2607 . . 3 class {𝑥 ∣ ∀𝑦 ¬ (𝑥𝑦𝑦 ≺ 𝒫 𝑥)}
152, 14cun 3570 . 2 class (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥𝑦𝑦 ≺ 𝒫 𝑥)})
161, 15wceq 1482 1 wff GCH = (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥𝑦𝑦 ≺ 𝒫 𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  elgch  9441  fingch  9442
  Copyright terms: Public domain W3C validator