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 | |- GCH = ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cgch | |- GCH |
|
1 | cfn | |- Fin |
|
2 | vx | |- x |
|
3 | vy | |- y |
|
4 | 2 | cv | |- x |
5 | csdm | |- ~< |
|
6 | 3 | cv | |- y |
7 | 4 6 5 | wbr | |- x ~< y |
8 | 4 | cpw | |- ~P x |
9 | 6 8 5 | wbr | |- y ~< ~P x |
10 | 7 9 | wa | |- ( x ~< y /\ y ~< ~P x ) |
11 | 10 | wn | |- -. ( x ~< y /\ y ~< ~P x ) |
12 | 11 3 | wal | |- A. y -. ( x ~< y /\ y ~< ~P x ) |
13 | 12 2 | cab | |- { x | A. y -. ( x ~< y /\ y ~< ~P x ) } |
14 | 1 13 | cun | |- ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } ) |
15 | 0 14 | wceq | |- GCH = ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } ) |