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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | djudoml | |
|
3 | 1 1 2 | syl2anc | |
4 | canth2g | |
|
5 | 4 | adantr | |
6 | sdomdom | |
|
7 | 5 6 | syl | |
8 | reldom | |
|
9 | 8 | brrelex1i | |
10 | djudom1 | |
|
11 | 9 10 | mpdan | |
12 | 9 | pwexd | |
13 | djudom2 | |
|
14 | 12 13 | mpdan | |
15 | domtr | |
|
16 | 11 14 15 | syl2anc | |
17 | 7 16 | syl | |
18 | pwdju1 | |
|
19 | 18 | adantr | |
20 | gchdju1 | |
|
21 | pwen | |
|
22 | 20 21 | syl | |
23 | entr | |
|
24 | 19 22 23 | syl2anc | |
25 | domentr | |
|
26 | 17 24 25 | syl2anc | |
27 | gchinf | |
|
28 | pwdjundom | |
|
29 | 27 28 | syl | |
30 | ensym | |
|
31 | endom | |
|
32 | 30 31 | syl | |
33 | 29 32 | nsyl | |
34 | brsdom | |
|
35 | 26 33 34 | sylanbrc | |
36 | 3 35 | jca | |
37 | gchen1 | |
|
38 | 36 37 | mpdan | |
39 | 38 | ensymd | |