Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-gch | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-gch | ⊢ GCH = (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cgch 9442 | . 2 class GCH | |
2 | cfn 7955 | . . 3 class Fin | |
3 | vx | . . . . . . . . 9 setvar 𝑥 | |
4 | 3 | cv 1482 | . . . . . . . 8 class 𝑥 |
5 | vy | . . . . . . . . 9 setvar 𝑦 | |
6 | 5 | cv 1482 | . . . . . . . 8 class 𝑦 |
7 | csdm 7954 | . . . . . . . 8 class ≺ | |
8 | 4, 6, 7 | wbr 4653 | . . . . . . 7 wff 𝑥 ≺ 𝑦 |
9 | 4 | cpw 4158 | . . . . . . . 8 class 𝒫 𝑥 |
10 | 6, 9, 7 | wbr 4653 | . . . . . . 7 wff 𝑦 ≺ 𝒫 𝑥 |
11 | 8, 10 | wa 384 | . . . . . 6 wff (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥) |
12 | 11 | wn 3 | . . . . 5 wff ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥) |
13 | 12, 5 | wal 1481 | . . . 4 wff ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥) |
14 | 13, 3 | cab 2608 | . . 3 class {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)} |
15 | 2, 14 | cun 3572 | . 2 class (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)}) |
16 | 1, 15 | wceq 1483 | 1 wff GCH = (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)}) |
Colors of variables: wff setvar class |
This definition is referenced by: elgch 9444 fingch 9445 |
Copyright terms: Public domain | W3C validator |