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

Definition df-gch 8928
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 8927 . 2  class GCH
2 cfn 7453 . . 3  class  Fin
3 vx . . . . . . . . 9  setvar  x
43cv 1398 . . . . . . . 8  class  x
5 vy . . . . . . . . 9  setvar  y
65cv 1398 . . . . . . . 8  class  y
7 csdm 7452 . . . . . . . 8  class  ~<
84, 6, 7wbr 4380 . . . . . . 7  wff  x  ~<  y
94cpw 3940 . . . . . . . 8  class  ~P x
106, 9, 7wbr 4380 . . . . . . 7  wff  y  ~<  ~P x
118, 10wa 367 . . . . . 6  wff  ( x 
~<  y  /\  y  ~<  ~P x )
1211wn 3 . . . . 5  wff  -.  (
x  ~<  y  /\  y  ~<  ~P x )
1312, 5wal 1397 . . . 4  wff  A. y  -.  ( x  ~<  y  /\  y  ~<  ~P x
)
1413, 3cab 2377 . . 3  class  { x  |  A. y  -.  (
x  ~<  y  /\  y  ~<  ~P x ) }
152, 14cun 3400 . 2  class  ( Fin 
u.  { x  | 
A. y  -.  (
x  ~<  y  /\  y  ~<  ~P x ) } )
161, 15wceq 1399 1  wff GCH  =  ( Fin  u.  { x  |  A. y  -.  (
x  ~<  y  /\  y  ~<  ~P x ) } )
Colors of variables: wff setvar class
This definition is referenced by:  elgch  8929  fingch  8930
  Copyright terms: Public domain W3C validator