Metamath Proof Explorer


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

Proof

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