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

Metamath Proof Explorer

Definition df-gch

Detailed syntax breakdown