gchen1

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

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

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

Metamath Proof Explorer