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

Definition df-gch 8497
 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 . 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.)
Assertion
Ref Expression
df-gch GCH
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-gch
StepHypRef Expression
1 cgch 8496 . 2 GCH
2 cfn 7110 . . 3
3 vx . . . . . . . . 9
43cv 1652 . . . . . . . 8
5 vy . . . . . . . . 9
65cv 1652 . . . . . . . 8
7 csdm 7109 . . . . . . . 8
84, 6, 7wbr 4213 . . . . . . 7
94cpw 3800 . . . . . . . 8
106, 9, 7wbr 4213 . . . . . . 7
118, 10wa 360 . . . . . 6
1211wn 3 . . . . 5
1312, 5wal 1550 . . . 4
1413, 3cab 2423 . . 3
152, 14cun 3319 . 2
161, 15wceq 1653 1 GCH
 Colors of variables: wff set class This definition is referenced by:  elgch  8498  fingch  8499
 Copyright terms: Public domain W3C validator