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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ex | |
|
2 | 1 | a1i | |
3 | xpsneng | |
|
4 | 2 3 | sylan2 | |
5 | 4 | ensymd | |
6 | df1o2 | |
|
7 | id | |
|
8 | 0fin | |
|
9 | 7 8 | eqeltrdi | |
10 | 9 | necon3bi | |
11 | 10 | adantl | |
12 | 0sdomg | |
|
13 | 12 | adantr | |
14 | 11 13 | mpbird | |
15 | 0sdom1dom | |
|
16 | 14 15 | sylib | |
17 | 6 16 | eqbrtrrid | |
18 | xpdom2g | |
|
19 | 17 18 | syldan | |
20 | endomtr | |
|
21 | 5 19 20 | syl2anc | |
22 | canth2g | |
|
23 | 22 | adantr | |
24 | sdomdom | |
|
25 | 23 24 | syl | |
26 | xpdom1g | |
|
27 | 25 26 | syldan | |
28 | pwexg | |
|
29 | 28 | adantr | |
30 | xpdom2g | |
|
31 | 29 25 30 | syl2anc | |
32 | domtr | |
|
33 | 27 31 32 | syl2anc | |
34 | simpl | |
|
35 | pwdjuen | |
|
36 | 34 35 | syldan | |
37 | 36 | ensymd | |
38 | gchdjuidm | |
|
39 | pwen | |
|
40 | 38 39 | syl | |
41 | entr | |
|
42 | 37 40 41 | syl2anc | |
43 | domentr | |
|
44 | 33 42 43 | syl2anc | |
45 | gchinf | |
|
46 | pwxpndom | |
|
47 | 45 46 | syl | |
48 | ensym | |
|
49 | endom | |
|
50 | 48 49 | syl | |
51 | 47 50 | nsyl | |
52 | brsdom | |
|
53 | 44 51 52 | sylanbrc | |
54 | 21 53 | jca | |
55 | gchen1 | |
|
56 | 54 55 | mpdan | |
57 | 56 | ensymd | |