gchxpidm

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

		Ref	Expression
	Assertion	gchxpidm	$⊢ (A \in GCH \land \neg A \in Fin) \to (A \times A) \approx A$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2	1	a1i	$⊢ \neg A \in Fin \to \emptyset \in V$
3		xpsneng	$⊢ (A \in GCH \land \emptyset \in V) \to (A \times \{\emptyset\}) \approx A$
4	2 3	sylan2	$⊢ (A \in GCH \land \neg A \in Fin) \to (A \times \{\emptyset\}) \approx A$
5	4	ensymd	$⊢ (A \in GCH \land \neg A \in Fin) \to A \approx (A \times \{\emptyset\})$
6		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
7		id	$⊢ A = \emptyset \to A = \emptyset$
8		0fin	$⊢ \emptyset \in Fin$
9	7 8	eqeltrdi	$⊢ A = \emptyset \to A \in Fin$
10	9	necon3bi	$⊢ \neg A \in Fin \to A \neq \emptyset$
11	10	adantl	$⊢ (A \in GCH \land \neg A \in Fin) \to A \neq \emptyset$
12		0sdomg	$⊢ A \in GCH \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
13	12	adantr	$⊢ (A \in GCH \land \neg A \in Fin) \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
14	11 13	mpbird	$⊢ (A \in GCH \land \neg A \in Fin) \to \emptyset ≺ A$
15		0sdom1dom	$⊢ \emptyset ≺ A \leftrightarrow 1_{𝑜} ≼ A$
16	14 15	sylib	$⊢ (A \in GCH \land \neg A \in Fin) \to 1_{𝑜} ≼ A$
17	6 16	eqbrtrrid	$⊢ (A \in GCH \land \neg A \in Fin) \to \{\emptyset\} ≼ A$
18		xpdom2g	$⊢ (A \in GCH \land \{\emptyset\} ≼ A) \to (A \times \{\emptyset\}) ≼ (A \times A)$
19	17 18	syldan	$⊢ (A \in GCH \land \neg A \in Fin) \to (A \times \{\emptyset\}) ≼ (A \times A)$
20		endomtr	$⊢ (A \approx (A \times \{\emptyset\}) \land (A \times \{\emptyset\}) ≼ (A \times A)) \to A ≼ (A \times A)$
21	5 19 20	syl2anc	$⊢ (A \in GCH \land \neg A \in Fin) \to A ≼ (A \times A)$
22		canth2g	$⊢ A \in GCH \to A ≺ 𝒫 A$
23	22	adantr	$⊢ (A \in GCH \land \neg A \in Fin) \to A ≺ 𝒫 A$
24		sdomdom	$⊢ A ≺ 𝒫 A \to A ≼ 𝒫 A$
25	23 24	syl	$⊢ (A \in GCH \land \neg A \in Fin) \to A ≼ 𝒫 A$
26		xpdom1g	$⊢ (A \in GCH \land A ≼ 𝒫 A) \to (A \times A) ≼ (𝒫 A \times A)$
27	25 26	syldan	$⊢ (A \in GCH \land \neg A \in Fin) \to (A \times A) ≼ (𝒫 A \times A)$
28		pwexg	$⊢ A \in GCH \to 𝒫 A \in V$
29	28	adantr	$⊢ (A \in GCH \land \neg A \in Fin) \to 𝒫 A \in V$
30		xpdom2g	$⊢ (𝒫 A \in V \land A ≼ 𝒫 A) \to (𝒫 A \times A) ≼ (𝒫 A \times 𝒫 A)$
31	29 25 30	syl2anc	$⊢ (A \in GCH \land \neg A \in Fin) \to (𝒫 A \times A) ≼ (𝒫 A \times 𝒫 A)$
32		domtr	$⊢ ((A \times A) ≼ (𝒫 A \times A) \land (𝒫 A \times A) ≼ (𝒫 A \times 𝒫 A)) \to (A \times A) ≼ (𝒫 A \times 𝒫 A)$
33	27 31 32	syl2anc	$⊢ (A \in GCH \land \neg A \in Fin) \to (A \times A) ≼ (𝒫 A \times 𝒫 A)$
34		simpl	$⊢ (A \in GCH \land \neg A \in Fin) \to A \in GCH$
35		pwdjuen	$⊢ (A \in GCH \land A \in GCH) \to 𝒫 (A ⊔︀ A) \approx (𝒫 A \times 𝒫 A)$
36	34 35	syldan	$⊢ (A \in GCH \land \neg A \in Fin) \to 𝒫 (A ⊔︀ A) \approx (𝒫 A \times 𝒫 A)$
37	36	ensymd	$⊢ (A \in GCH \land \neg A \in Fin) \to (𝒫 A \times 𝒫 A) \approx 𝒫 (A ⊔︀ A)$
38		gchdjuidm	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ A) \approx A$
39		pwen	$⊢ (A ⊔︀ A) \approx A \to 𝒫 (A ⊔︀ A) \approx 𝒫 A$
40	38 39	syl	$⊢ (A \in GCH \land \neg A \in Fin) \to 𝒫 (A ⊔︀ A) \approx 𝒫 A$
41		entr	$⊢ ((𝒫 A \times 𝒫 A) \approx 𝒫 (A ⊔︀ A) \land 𝒫 (A ⊔︀ A) \approx 𝒫 A) \to (𝒫 A \times 𝒫 A) \approx 𝒫 A$
42	37 40 41	syl2anc	$⊢ (A \in GCH \land \neg A \in Fin) \to (𝒫 A \times 𝒫 A) \approx 𝒫 A$
43		domentr	$⊢ ((A \times A) ≼ (𝒫 A \times 𝒫 A) \land (𝒫 A \times 𝒫 A) \approx 𝒫 A) \to (A \times A) ≼ 𝒫 A$
44	33 42 43	syl2anc	$⊢ (A \in GCH \land \neg A \in Fin) \to (A \times A) ≼ 𝒫 A$
45		gchinf	$⊢ (A \in GCH \land \neg A \in Fin) \to ω ≼ A$
46		pwxpndom	$⊢ ω ≼ A \to \neg 𝒫 A ≼ (A \times A)$
47	45 46	syl	$⊢ (A \in GCH \land \neg A \in Fin) \to \neg 𝒫 A ≼ (A \times A)$
48		ensym	$⊢ (A \times A) \approx 𝒫 A \to 𝒫 A \approx (A \times A)$
49		endom	$⊢ 𝒫 A \approx (A \times A) \to 𝒫 A ≼ (A \times A)$
50	48 49	syl	$⊢ (A \times A) \approx 𝒫 A \to 𝒫 A ≼ (A \times A)$
51	47 50	nsyl	$⊢ (A \in GCH \land \neg A \in Fin) \to \neg (A \times A) \approx 𝒫 A$
52		brsdom	$⊢ (A \times A) ≺ 𝒫 A \leftrightarrow ((A \times A) ≼ 𝒫 A \land \neg (A \times A) \approx 𝒫 A)$
53	44 51 52	sylanbrc	$⊢ (A \in GCH \land \neg A \in Fin) \to (A \times A) ≺ 𝒫 A$
54	21 53	jca	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ≼ (A \times A) \land (A \times A) ≺ 𝒫 A)$
55		gchen1	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≼ (A \times A) \land (A \times A) ≺ 𝒫 A)) \to A \approx (A \times A)$
56	54 55	mpdan	$⊢ (A \in GCH \land \neg A \in Fin) \to A \approx (A \times A)$
57	56	ensymd	$⊢ (A \in GCH \land \neg A \in Fin) \to (A \times A) \approx A$

Metamath Proof Explorer

Theorem gchxpidm

Proof