gchen2

Description: If A < B <_ ~P A , and A is an infinite GCH-set, then B = ~P A in cardinality. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	gchen2	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≺ B \land B ≼ 𝒫 A)) \to B \approx 𝒫 A$

Step	Hyp	Ref	Expression
1		simprr	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≺ B \land B ≼ 𝒫 A)) \to B ≼ 𝒫 A$
2		gchi	$⊢ (A \in GCH \land A ≺ B \land B ≺ 𝒫 A) \to A \in Fin$
3	2	3expia	$⊢ (A \in GCH \land A ≺ B) \to (B ≺ 𝒫 A \to A \in Fin)$
4	3	con3dimp	$⊢ ((A \in GCH \land A ≺ B) \land \neg A \in Fin) \to \neg B ≺ 𝒫 A$
5	4	an32s	$⊢ ((A \in GCH \land \neg A \in Fin) \land A ≺ B) \to \neg B ≺ 𝒫 A$
6	5	adantrr	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≺ B \land B ≼ 𝒫 A)) \to \neg B ≺ 𝒫 A$
7		bren2	$⊢ B \approx 𝒫 A \leftrightarrow (B ≼ 𝒫 A \land \neg B ≺ 𝒫 A)$
8	1 6 7	sylanbrc	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≺ B \land B ≼ 𝒫 A)) \to B \approx 𝒫 A$

Metamath Proof Explorer