Metamath Proof Explorer

Theorem engch

Description: The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	engch	$⊢ A \approx B \to (A \in GCH \leftrightarrow B \in GCH)$

Proof

Step	Hyp	Ref	Expression
1		enfi	$⊢ A \approx B \to (A \in Fin \leftrightarrow B \in Fin)$
2		sdomen1	$⊢ A \approx B \to (A ≺ x \leftrightarrow B ≺ x)$
3		pwen	$⊢ A \approx B \to 𝒫 A \approx 𝒫 B$
4		sdomen2	$⊢ 𝒫 A \approx 𝒫 B \to (x ≺ 𝒫 A \leftrightarrow x ≺ 𝒫 B)$
5	3 4	syl	$⊢ A \approx B \to (x ≺ 𝒫 A \leftrightarrow x ≺ 𝒫 B)$
6	2 5	anbi12d	$⊢ A \approx B \to ((A ≺ x \land x ≺ 𝒫 A) \leftrightarrow (B ≺ x \land x ≺ 𝒫 B))$
7	6	notbid	$⊢ A \approx B \to (\neg (A ≺ x \land x ≺ 𝒫 A) \leftrightarrow \neg (B ≺ x \land x ≺ 𝒫 B))$
8	7	albidv	$⊢ A \approx B \to (\forall x \neg (A ≺ x \land x ≺ 𝒫 A) \leftrightarrow \forall x \neg (B ≺ x \land x ≺ 𝒫 B))$
9	1 8	orbi12d	$⊢ A \approx B \to ((A \in Fin \lor \forall x \neg (A ≺ x \land x ≺ 𝒫 A)) \leftrightarrow (B \in Fin \lor \forall x \neg (B ≺ x \land x ≺ 𝒫 B)))$
10		relen	$⊢ Rel \approx$
11	10	brrelex1i	$⊢ A \approx B \to A \in V$
12		elgch	$⊢ A \in V \to (A \in GCH \leftrightarrow (A \in Fin \lor \forall x \neg (A ≺ x \land x ≺ 𝒫 A)))$
13	11 12	syl	$⊢ A \approx B \to (A \in GCH \leftrightarrow (A \in Fin \lor \forall x \neg (A ≺ x \land x ≺ 𝒫 A)))$
14	10	brrelex2i	$⊢ A \approx B \to B \in V$
15		elgch	$⊢ B \in V \to (B \in GCH \leftrightarrow (B \in Fin \lor \forall x \neg (B ≺ x \land x ≺ 𝒫 B)))$
16	14 15	syl	$⊢ A \approx B \to (B \in GCH \leftrightarrow (B \in Fin \lor \forall x \neg (B ≺ x \land x ≺ 𝒫 B)))$
17	9 13 16	3bitr4d	$⊢ A \approx B \to (A \in GCH \leftrightarrow B \in GCH)$