This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ( 𝐴 ⊔ 𝐴 ) ≈ 𝐴 )