gchdjuidm

Description: An infinite GCH-set is idempotent under cardinal sum. Part of Lemma 2.2 of KanamoriPincus p. 419. (Contributed by Mario Carneiro, 31-May-2015)

		Ref	Expression
	Assertion	gchdjuidm	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ A) \approx A$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in GCH \land \neg A \in Fin) \to A \in GCH$
2		djudoml	$⊢ (A \in GCH \land A \in GCH) \to A ≼ (A ⊔︀ A)$
3	1 1 2	syl2anc	$⊢ (A \in GCH \land \neg A \in Fin) \to A ≼ (A ⊔︀ A)$
4		canth2g	$⊢ A \in GCH \to A ≺ 𝒫 A$
5	4	adantr	$⊢ (A \in GCH \land \neg A \in Fin) \to A ≺ 𝒫 A$
6		sdomdom	$⊢ A ≺ 𝒫 A \to A ≼ 𝒫 A$
7	5 6	syl	$⊢ (A \in GCH \land \neg A \in Fin) \to A ≼ 𝒫 A$
8		reldom	$⊢ Rel ≼$
9	8	brrelex1i	$⊢ A ≼ 𝒫 A \to A \in V$
10		djudom1	$⊢ (A ≼ 𝒫 A \land A \in V) \to (A ⊔︀ A) ≼ (𝒫 A ⊔︀ A)$
11	9 10	mpdan	$⊢ A ≼ 𝒫 A \to (A ⊔︀ A) ≼ (𝒫 A ⊔︀ A)$
12	9	pwexd	$⊢ A ≼ 𝒫 A \to 𝒫 A \in V$
13		djudom2	$⊢ (A ≼ 𝒫 A \land 𝒫 A \in V) \to (𝒫 A ⊔︀ A) ≼ (𝒫 A ⊔︀ 𝒫 A)$
14	12 13	mpdan	$⊢ A ≼ 𝒫 A \to (𝒫 A ⊔︀ A) ≼ (𝒫 A ⊔︀ 𝒫 A)$
15		domtr	$⊢ ((A ⊔︀ A) ≼ (𝒫 A ⊔︀ A) \land (𝒫 A ⊔︀ A) ≼ (𝒫 A ⊔︀ 𝒫 A)) \to (A ⊔︀ A) ≼ (𝒫 A ⊔︀ 𝒫 A)$
16	11 14 15	syl2anc	$⊢ A ≼ 𝒫 A \to (A ⊔︀ A) ≼ (𝒫 A ⊔︀ 𝒫 A)$
17	7 16	syl	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ A) ≼ (𝒫 A ⊔︀ 𝒫 A)$
18		pwdju1	$⊢ A \in GCH \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 (A ⊔︀ 1_{𝑜})$
19	18	adantr	$⊢ (A \in GCH \land \neg A \in Fin) \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 (A ⊔︀ 1_{𝑜})$
20		gchdju1	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ 1_{𝑜}) \approx A$
21		pwen	$⊢ (A ⊔︀ 1_{𝑜}) \approx A \to 𝒫 (A ⊔︀ 1_{𝑜}) \approx 𝒫 A$
22	20 21	syl	$⊢ (A \in GCH \land \neg A \in Fin) \to 𝒫 (A ⊔︀ 1_{𝑜}) \approx 𝒫 A$
23		entr	$⊢ ((𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 (A ⊔︀ 1_{𝑜}) \land 𝒫 (A ⊔︀ 1_{𝑜}) \approx 𝒫 A) \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 A$
24	19 22 23	syl2anc	$⊢ (A \in GCH \land \neg A \in Fin) \to (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 A$
25		domentr	$⊢ ((A ⊔︀ A) ≼ (𝒫 A ⊔︀ 𝒫 A) \land (𝒫 A ⊔︀ 𝒫 A) \approx 𝒫 A) \to (A ⊔︀ A) ≼ 𝒫 A$
26	17 24 25	syl2anc	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ A) ≼ 𝒫 A$
27		gchinf	$⊢ (A \in GCH \land \neg A \in Fin) \to ω ≼ A$
28		pwdjundom	$⊢ ω ≼ A \to \neg 𝒫 A ≼ (A ⊔︀ A)$
29	27 28	syl	$⊢ (A \in GCH \land \neg A \in Fin) \to \neg 𝒫 A ≼ (A ⊔︀ A)$
30		ensym	$⊢ (A ⊔︀ A) \approx 𝒫 A \to 𝒫 A \approx (A ⊔︀ A)$
31		endom	$⊢ 𝒫 A \approx (A ⊔︀ A) \to 𝒫 A ≼ (A ⊔︀ A)$
32	30 31	syl	$⊢ (A ⊔︀ A) \approx 𝒫 A \to 𝒫 A ≼ (A ⊔︀ A)$
33	29 32	nsyl	$⊢ (A \in GCH \land \neg A \in Fin) \to \neg (A ⊔︀ A) \approx 𝒫 A$
34		brsdom	$⊢ (A ⊔︀ A) ≺ 𝒫 A \leftrightarrow ((A ⊔︀ A) ≼ 𝒫 A \land \neg (A ⊔︀ A) \approx 𝒫 A)$
35	26 33 34	sylanbrc	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ A) ≺ 𝒫 A$
36	3 35	jca	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ≼ (A ⊔︀ A) \land (A ⊔︀ A) ≺ 𝒫 A)$
37		gchen1	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≼ (A ⊔︀ A) \land (A ⊔︀ A) ≺ 𝒫 A)) \to A \approx (A ⊔︀ A)$
38	36 37	mpdan	$⊢ (A \in GCH \land \neg A \in Fin) \to A \approx (A ⊔︀ A)$
39	38	ensymd	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ A) \approx A$

Metamath Proof Explorer

Theorem gchdjuidm

Proof