Metamath Proof Explorer


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
|- GCH = ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )

Detailed syntax breakdown

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 ) } )