gchi

Description: The only GCH-sets which have other sets between it and its power set are finite sets. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	gchi	$⊢ (A \in GCH \land A ≺ B \land B ≺ 𝒫 A) \to A \in Fin$

Step	Hyp	Ref	Expression
1		relsdom	$⊢ Rel ≺$
2	1	brrelex1i	$⊢ B ≺ 𝒫 A \to B \in V$
3	2	adantl	$⊢ (A ≺ B \land B ≺ 𝒫 A) \to B \in V$
4		breq2	$⊢ x = B \to (A ≺ x \leftrightarrow A ≺ B)$
5		breq1	$⊢ x = B \to (x ≺ 𝒫 A \leftrightarrow B ≺ 𝒫 A)$
6	4 5	anbi12d	$⊢ x = B \to ((A ≺ x \land x ≺ 𝒫 A) \leftrightarrow (A ≺ B \land B ≺ 𝒫 A))$
7	6	spcegv	$⊢ B \in V \to ((A ≺ B \land B ≺ 𝒫 A) \to \exists x (A ≺ x \land x ≺ 𝒫 A))$
8	3 7	mpcom	$⊢ (A ≺ B \land B ≺ 𝒫 A) \to \exists x (A ≺ x \land x ≺ 𝒫 A)$
9		df-ex	$⊢ \exists x (A ≺ x \land x ≺ 𝒫 A) \leftrightarrow \neg \forall x \neg (A ≺ x \land x ≺ 𝒫 A)$
10	8 9	sylib	$⊢ (A ≺ B \land B ≺ 𝒫 A) \to \neg \forall x \neg (A ≺ x \land x ≺ 𝒫 A)$
11		elgch	$⊢ A \in GCH \to (A \in GCH \leftrightarrow (A \in Fin \lor \forall x \neg (A ≺ x \land x ≺ 𝒫 A)))$
12	11	ibi	$⊢ A \in GCH \to (A \in Fin \lor \forall x \neg (A ≺ x \land x ≺ 𝒫 A))$
13	12	orcomd	$⊢ A \in GCH \to (\forall x \neg (A ≺ x \land x ≺ 𝒫 A) \lor A \in Fin)$
14	13	ord	$⊢ A \in GCH \to (\neg \forall x \neg (A ≺ x \land x ≺ 𝒫 A) \to A \in Fin)$
15	10 14	syl5	$⊢ A \in GCH \to ((A ≺ B \land B ≺ 𝒫 A) \to A \in Fin)$
16	15	3impib	$⊢ (A \in GCH \land A ≺ B \land B ≺ 𝒫 A) \to A \in Fin$

Metamath Proof Explorer