gchdju1

Description: An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015)

		Ref	Expression
	Assertion	gchdju1	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ 1_{𝑜}) \approx A$

Proof

Step	Hyp	Ref	Expression
1		1onn	$⊢ 1_{𝑜} \in ω$
2	1	a1i	$⊢ \neg A \in Fin \to 1_{𝑜} \in ω$
3		djudoml	$⊢ (A \in GCH \land 1_{𝑜} \in ω) \to A ≼ (A ⊔︀ 1_{𝑜})$
4	2 3	sylan2	$⊢ (A \in GCH \land \neg A \in Fin) \to A ≼ (A ⊔︀ 1_{𝑜})$
5		simpr	$⊢ (A \in GCH \land \neg A \in Fin) \to \neg A \in Fin$
6		nnfi	$⊢ 1_{𝑜} \in ω \to 1_{𝑜} \in Fin$
7	1 6	mp1i	$⊢ \neg A \in Fin \to 1_{𝑜} \in Fin$
8		fidomtri2	$⊢ (A \in GCH \land 1_{𝑜} \in Fin) \to (A ≼ 1_{𝑜} \leftrightarrow \neg 1_{𝑜} ≺ A)$
9	7 8	sylan2	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ≼ 1_{𝑜} \leftrightarrow \neg 1_{𝑜} ≺ A)$
10	1 6	mp1i	$⊢ (A \in GCH \land \neg A \in Fin) \to 1_{𝑜} \in Fin$
11		domfi	$⊢ (1_{𝑜} \in Fin \land A ≼ 1_{𝑜}) \to A \in Fin$
12	11	ex	$⊢ 1_{𝑜} \in Fin \to (A ≼ 1_{𝑜} \to A \in Fin)$
13	10 12	syl	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ≼ 1_{𝑜} \to A \in Fin)$
14	9 13	sylbird	$⊢ (A \in GCH \land \neg A \in Fin) \to (\neg 1_{𝑜} ≺ A \to A \in Fin)$
15	5 14	mt3d	$⊢ (A \in GCH \land \neg A \in Fin) \to 1_{𝑜} ≺ A$
16		canthp1	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 1_{𝑜}) ≺ 𝒫 A$
17	15 16	syl	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ 1_{𝑜}) ≺ 𝒫 A$
18	4 17	jca	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ≼ (A ⊔︀ 1_{𝑜}) \land (A ⊔︀ 1_{𝑜}) ≺ 𝒫 A)$
19		gchen1	$⊢ ((A \in GCH \land \neg A \in Fin) \land (A ≼ (A ⊔︀ 1_{𝑜}) \land (A ⊔︀ 1_{𝑜}) ≺ 𝒫 A)) \to A \approx (A ⊔︀ 1_{𝑜})$
20	18 19	mpdan	$⊢ (A \in GCH \land \neg A \in Fin) \to A \approx (A ⊔︀ 1_{𝑜})$
21	20	ensymd	$⊢ (A \in GCH \land \neg A \in Fin) \to (A ⊔︀ 1_{𝑜}) \approx A$

Metamath Proof Explorer

Theorem gchdju1

Proof