Theorem gchdju1

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

	Ref	Expression
Assertion	gchdju1	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		1onn	⊢ 1o ∈ ω
2	1	a1i	⊢ ( ¬ 𝐴 ∈ Fin → 1o ∈ ω )
3		djudoml	⊢ ( ( 𝐴 ∈ GCH ∧ 1o ∈ ω ) → 𝐴 ≼ ( 𝐴 ⊔ 1o ) )
4	2 3	sylan2	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≼ ( 𝐴 ⊔ 1o ) )
5		simpr	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ¬ 𝐴 ∈ Fin )
6		nnfi	⊢ ( 1o ∈ ω → 1o ∈ Fin )
7	1 6	mp1i	⊢ ( ¬ 𝐴 ∈ Fin → 1o ∈ Fin )
8		fidomtri2	⊢ ( ( 𝐴 ∈ GCH ∧ 1o ∈ Fin ) → ( 𝐴 ≼ 1o ↔ ¬ 1o ≺ 𝐴 ) )
9	7 8	sylan2	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ≼ 1o ↔ ¬ 1o ≺ 𝐴 ) )
10	1 6	mp1i	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 1o ∈ Fin )
11		domfi	⊢ ( ( 1o ∈ Fin ∧ 𝐴 ≼ 1o ) → 𝐴 ∈ Fin )
12	11	ex	⊢ ( 1o ∈ Fin → ( 𝐴 ≼ 1o → 𝐴 ∈ Fin ) )
13	10 12	syl	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ≼ 1o → 𝐴 ∈ Fin ) )
14	9 13	sylbird	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( ¬ 1o ≺ 𝐴 → 𝐴 ∈ Fin ) )
15	5 14	mt3d	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 1o ≺ 𝐴 )
16		canthp1	⊢ ( 1o ≺ 𝐴 → ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 )
17	15 16	syl	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 )
18	4 17	jca	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ≼ ( 𝐴 ⊔ 1o ) ∧ ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 ) )
19		gchen1	⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ ( 𝐴 ⊔ 1o ) ∧ ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 ) ) → 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
20	18 19	mpdan	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
21	20	ensymd	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )