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

Definition df-gch 8259
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.)
Assertion
Ref Expression
df-gch  |- GCH  =  ( Fin  u.  { x  |  A. y  -.  (
x  ~<  y  /\  y  ~<  ~P x ) } )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-gch
StepHypRef Expression
1 cgch 8258 . 2  class GCH
2 cfn 6879 . . 3  class  Fin
3 vx . . . . . . . . 9  set  x
43cv 1631 . . . . . . . 8  class  x
5 vy . . . . . . . . 9  set  y
65cv 1631 . . . . . . . 8  class  y
7 csdm 6878 . . . . . . . 8  class  ~<
84, 6, 7wbr 4039 . . . . . . 7  wff  x  ~<  y
94cpw 3638 . . . . . . . 8  class  ~P x
106, 9, 7wbr 4039 . . . . . . 7  wff  y  ~<  ~P x
118, 10wa 358 . . . . . 6  wff  ( x 
~<  y  /\  y  ~<  ~P x )
1211wn 3 . . . . 5  wff  -.  (
x  ~<  y  /\  y  ~<  ~P x )
1312, 5wal 1530 . . . 4  wff  A. y  -.  ( x  ~<  y  /\  y  ~<  ~P x
)
1413, 3cab 2282 . . 3  class  { x  |  A. y  -.  (
x  ~<  y  /\  y  ~<  ~P x ) }
152, 14cun 3163 . 2  class  ( Fin 
u.  { x  | 
A. y  -.  (
x  ~<  y  /\  y  ~<  ~P x ) } )
161, 15wceq 1632 1  wff GCH  =  ( Fin  u.  { x  |  A. y  -.  (
x  ~<  y  /\  y  ~<  ~P x ) } )
Colors of variables: wff set class
This definition is referenced by:  elgch  8260  fingch  8261
  Copyright terms: Public domain W3C validator