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

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 0fi ⊢ ∅ ∈ 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 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )