Theorem 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	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ∈ GCH )
2		djudoml	⊢ ( ( 𝐴 ∈ GCH ∧ 𝐴 ∈ GCH ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )
3	1 1 2	syl2anc	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )
4		canth2g	⊢ ( 𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴 )
5	4	adantr	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≺ 𝒫 𝐴 )
6		sdomdom	⊢ ( 𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴 )
7	5 6	syl	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≼ 𝒫 𝐴 )
8		reldom	⊢ Rel ≼
9	8	brrelex1i	⊢ ( 𝐴 ≼ 𝒫 𝐴 → 𝐴 ∈ V )
10		djudom1	⊢ ( ( 𝐴 ≼ 𝒫 𝐴 ∧ 𝐴 ∈ V ) → ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝒫 𝐴 ⊔ 𝐴 ) )
11	9 10	mpdan	⊢ ( 𝐴 ≼ 𝒫 𝐴 → ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝒫 𝐴 ⊔ 𝐴 ) )
12	9	pwexd	⊢ ( 𝐴 ≼ 𝒫 𝐴 → 𝒫 𝐴 ∈ V )
13		djudom2	⊢ ( ( 𝐴 ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ V ) → ( 𝒫 𝐴 ⊔ 𝐴 ) ≼ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
14	12 13	mpdan	⊢ ( 𝐴 ≼ 𝒫 𝐴 → ( 𝒫 𝐴 ⊔ 𝐴 ) ≼ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
15		domtr	⊢ ( ( ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝒫 𝐴 ⊔ 𝐴 ) ∧ ( 𝒫 𝐴 ⊔ 𝐴 ) ≼ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ) → ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
16	11 14 15	syl2anc	⊢ ( 𝐴 ≼ 𝒫 𝐴 → ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
17	7 16	syl	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) )
18		pwdju1	⊢ ( 𝐴 ∈ GCH → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 ( 𝐴 ⊔ 1o ) )
19	18	adantr	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 ( 𝐴 ⊔ 1o ) )
20		gchdju1	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )
21		pwen	⊢ ( ( 𝐴 ⊔ 1o ) ≈ 𝐴 → 𝒫 ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 )
22	20 21	syl	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝒫 ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 )
23		entr	⊢ ( ( ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 ( 𝐴 ⊔ 1o ) ∧ 𝒫 ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 ) → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 𝐴 )
24	19 22 23	syl2anc	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 𝐴 )
25		domentr	⊢ ( ( ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ∧ ( 𝒫 𝐴 ⊔ 𝒫 𝐴 ) ≈ 𝒫 𝐴 ) → ( 𝐴 ⊔ 𝐴 ) ≼ 𝒫 𝐴 )
26	17 24 25	syl2anc	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 𝐴 ) ≼ 𝒫 𝐴 )
27		gchinf	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ω ≼ 𝐴 )
28		pwdjundom	⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )
29	27 28	syl	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )
30		ensym	⊢ ( ( 𝐴 ⊔ 𝐴 ) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≈ ( 𝐴 ⊔ 𝐴 ) )
31		endom	⊢ ( 𝒫 𝐴 ≈ ( 𝐴 ⊔ 𝐴 ) → 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )
32	30 31	syl	⊢ ( ( 𝐴 ⊔ 𝐴 ) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )
33	29 32	nsyl	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ¬ ( 𝐴 ⊔ 𝐴 ) ≈ 𝒫 𝐴 )
34		brsdom	⊢ ( ( 𝐴 ⊔ 𝐴 ) ≺ 𝒫 𝐴 ↔ ( ( 𝐴 ⊔ 𝐴 ) ≼ 𝒫 𝐴 ∧ ¬ ( 𝐴 ⊔ 𝐴 ) ≈ 𝒫 𝐴 ) )
35	26 33 34	sylanbrc	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 𝐴 ) ≺ 𝒫 𝐴 )
36	3 35	jca	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) ∧ ( 𝐴 ⊔ 𝐴 ) ≺ 𝒫 𝐴 ) )
37		gchen1	⊢ ( ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) ∧ ( 𝐴 ⊔ 𝐴 ) ≺ 𝒫 𝐴 ) ) → 𝐴 ≈ ( 𝐴 ⊔ 𝐴 ) )
38	36 37	mpdan	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ≈ ( 𝐴 ⊔ 𝐴 ) )
39	38	ensymd	⊢ ( ( 𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin ) → ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 )