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 ∪ { 𝑥 ∣ ∀ 𝑦 ¬ ( 𝑥𝑦𝑦 ≺ 𝒫 𝑥 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgch GCH
1 cfn Fin
2 vx 𝑥
3 vy 𝑦
4 2 cv 𝑥
5 csdm
6 3 cv 𝑦
7 4 6 5 wbr 𝑥𝑦
8 4 cpw 𝒫 𝑥
9 6 8 5 wbr 𝑦 ≺ 𝒫 𝑥
10 7 9 wa ( 𝑥𝑦𝑦 ≺ 𝒫 𝑥 )
11 10 wn ¬ ( 𝑥𝑦𝑦 ≺ 𝒫 𝑥 )
12 11 3 wal 𝑦 ¬ ( 𝑥𝑦𝑦 ≺ 𝒫 𝑥 )
13 12 2 cab { 𝑥 ∣ ∀ 𝑦 ¬ ( 𝑥𝑦𝑦 ≺ 𝒫 𝑥 ) }
14 1 13 cun ( Fin ∪ { 𝑥 ∣ ∀ 𝑦 ¬ ( 𝑥𝑦𝑦 ≺ 𝒫 𝑥 ) } )
15 0 14 wceq GCH = ( Fin ∪ { 𝑥 ∣ ∀ 𝑦 ¬ ( 𝑥𝑦𝑦 ≺ 𝒫 𝑥 ) } )