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 AGCH¬AFinA⊔︀AA

Proof

Step Hyp Ref Expression
1 simpl AGCH¬AFinAGCH
2 djudoml AGCHAGCHAA⊔︀A
3 1 1 2 syl2anc AGCH¬AFinAA⊔︀A
4 canth2g AGCHA𝒫A
5 4 adantr AGCH¬AFinA𝒫A
6 sdomdom A𝒫AA𝒫A
7 5 6 syl AGCH¬AFinA𝒫A
8 reldom Rel
9 8 brrelex1i A𝒫AAV
10 djudom1 A𝒫AAVA⊔︀A𝒫A⊔︀A
11 9 10 mpdan A𝒫AA⊔︀A𝒫A⊔︀A
12 9 pwexd A𝒫A𝒫AV
13 djudom2 A𝒫A𝒫AV𝒫A⊔︀A𝒫A⊔︀𝒫A
14 12 13 mpdan A𝒫A𝒫A⊔︀A𝒫A⊔︀𝒫A
15 domtr A⊔︀A𝒫A⊔︀A𝒫A⊔︀A𝒫A⊔︀𝒫AA⊔︀A𝒫A⊔︀𝒫A
16 11 14 15 syl2anc A𝒫AA⊔︀A𝒫A⊔︀𝒫A
17 7 16 syl AGCH¬AFinA⊔︀A𝒫A⊔︀𝒫A
18 pwdju1 AGCH𝒫A⊔︀𝒫A𝒫A⊔︀1𝑜
19 18 adantr AGCH¬AFin𝒫A⊔︀𝒫A𝒫A⊔︀1𝑜
20 gchdju1 AGCH¬AFinA⊔︀1𝑜A
21 pwen A⊔︀1𝑜A𝒫A⊔︀1𝑜𝒫A
22 20 21 syl AGCH¬AFin𝒫A⊔︀1𝑜𝒫A
23 entr 𝒫A⊔︀𝒫A𝒫A⊔︀1𝑜𝒫A⊔︀1𝑜𝒫A𝒫A⊔︀𝒫A𝒫A
24 19 22 23 syl2anc AGCH¬AFin𝒫A⊔︀𝒫A𝒫A
25 domentr A⊔︀A𝒫A⊔︀𝒫A𝒫A⊔︀𝒫A𝒫AA⊔︀A𝒫A
26 17 24 25 syl2anc AGCH¬AFinA⊔︀A𝒫A
27 gchinf AGCH¬AFinωA
28 pwdjundom ωA¬𝒫AA⊔︀A
29 27 28 syl AGCH¬AFin¬𝒫AA⊔︀A
30 ensym A⊔︀A𝒫A𝒫AA⊔︀A
31 endom 𝒫AA⊔︀A𝒫AA⊔︀A
32 30 31 syl A⊔︀A𝒫A𝒫AA⊔︀A
33 29 32 nsyl AGCH¬AFin¬A⊔︀A𝒫A
34 brsdom A⊔︀A𝒫AA⊔︀A𝒫A¬A⊔︀A𝒫A
35 26 33 34 sylanbrc AGCH¬AFinA⊔︀A𝒫A
36 3 35 jca AGCH¬AFinAA⊔︀AA⊔︀A𝒫A
37 gchen1 AGCH¬AFinAA⊔︀AA⊔︀A𝒫AAA⊔︀A
38 36 37 mpdan AGCH¬AFinAA⊔︀A
39 38 ensymd AGCH¬AFinA⊔︀AA