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

Definition df-gch 9020
 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 . 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 . (Contributed by Mario Carneiro, 15-May-2015.)
Assertion
Ref Expression
df-gch
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-gch
StepHypRef Expression
1 cgch 9019 . 2
2 cfn 7536 . . 3
3 vx . . . . . . . . 9
43cv 1394 . . . . . . . 8
5 vy . . . . . . . . 9
65cv 1394 . . . . . . . 8
7 csdm 7535 . . . . . . . 8
84, 6, 7wbr 4452 . . . . . . 7
94cpw 4012 . . . . . . . 8
106, 9, 7wbr 4452 . . . . . . 7
118, 10wa 369 . . . . . 6
1211wn 3 . . . . 5
1312, 5wal 1393 . . . 4
1413, 3cab 2442 . . 3
152, 14cun 3473 . 2
161, 15wceq 1395 1
 Colors of variables: wff setvar class This definition is referenced by:  elgch  9021  fingch  9022
 Copyright terms: Public domain W3C validator