This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gchor

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

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

Proof

Step	Hyp	Ref	Expression
1		simprr	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≼ B \land B ≼ 𝒫 A)) \to B ≼ 𝒫 A$
2		brdom2	$⊢ B ≼ 𝒫 A \leftrightarrow (B ≺ 𝒫 A \lor B \approx 𝒫 A)$
3	1 2	sylib	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≼ B \land B ≼ 𝒫 A)) \to (B ≺ 𝒫 A \lor B \approx 𝒫 A)$
4		gchen1	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≼ B \land B ≺ 𝒫 A)) \to A \approx B$
5	4	expr	$⊢ ((A \in GCH \land \neg A \in Fin) \land A ≼ B) \to (B ≺ 𝒫 A \to A \approx B)$
6	5	adantrr	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≼ B \land B ≼ 𝒫 A)) \to (B ≺ 𝒫 A \to A \approx B)$
7	6	orim1d	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≼ B \land B ≼ 𝒫 A)) \to ((B ≺ 𝒫 A \lor B \approx 𝒫 A) \to (A \approx B \lor B \approx 𝒫 A))$
8	3 7	mpd	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≼ B \land B ≼ 𝒫 A)) \to (A \approx B \lor B \approx 𝒫 A)$