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

Proof

Step Hyp Ref Expression
1 0ex V
2 1 a1i ¬AFinV
3 xpsneng AGCHVA×A
4 2 3 sylan2 AGCH¬AFinA×A
5 4 ensymd AGCH¬AFinAA×
6 df1o2 1𝑜=
7 id A=A=
8 0fin Fin
9 7 8 eqeltrdi A=AFin
10 9 necon3bi ¬AFinA
11 10 adantl AGCH¬AFinA
12 0sdomg AGCHAA
13 12 adantr AGCH¬AFinAA
14 11 13 mpbird AGCH¬AFinA
15 0sdom1dom A1𝑜A
16 14 15 sylib AGCH¬AFin1𝑜A
17 6 16 eqbrtrrid AGCH¬AFinA
18 xpdom2g AGCHAA×A×A
19 17 18 syldan AGCH¬AFinA×A×A
20 endomtr AA×A×A×AAA×A
21 5 19 20 syl2anc AGCH¬AFinAA×A
22 canth2g AGCHA𝒫A
23 22 adantr AGCH¬AFinA𝒫A
24 sdomdom A𝒫AA𝒫A
25 23 24 syl AGCH¬AFinA𝒫A
26 xpdom1g AGCHA𝒫AA×A𝒫A×A
27 25 26 syldan AGCH¬AFinA×A𝒫A×A
28 pwexg AGCH𝒫AV
29 28 adantr AGCH¬AFin𝒫AV
30 xpdom2g 𝒫AVA𝒫A𝒫A×A𝒫A×𝒫A
31 29 25 30 syl2anc AGCH¬AFin𝒫A×A𝒫A×𝒫A
32 domtr A×A𝒫A×A𝒫A×A𝒫A×𝒫AA×A𝒫A×𝒫A
33 27 31 32 syl2anc AGCH¬AFinA×A𝒫A×𝒫A
34 simpl AGCH¬AFinAGCH
35 pwdjuen AGCHAGCH𝒫A⊔︀A𝒫A×𝒫A
36 34 35 syldan AGCH¬AFin𝒫A⊔︀A𝒫A×𝒫A
37 36 ensymd AGCH¬AFin𝒫A×𝒫A𝒫A⊔︀A
38 gchdjuidm AGCH¬AFinA⊔︀AA
39 pwen A⊔︀AA𝒫A⊔︀A𝒫A
40 38 39 syl AGCH¬AFin𝒫A⊔︀A𝒫A
41 entr 𝒫A×𝒫A𝒫A⊔︀A𝒫A⊔︀A𝒫A𝒫A×𝒫A𝒫A
42 37 40 41 syl2anc AGCH¬AFin𝒫A×𝒫A𝒫A
43 domentr A×A𝒫A×𝒫A𝒫A×𝒫A𝒫AA×A𝒫A
44 33 42 43 syl2anc AGCH¬AFinA×A𝒫A
45 gchinf AGCH¬AFinωA
46 pwxpndom ωA¬𝒫AA×A
47 45 46 syl AGCH¬AFin¬𝒫AA×A
48 ensym A×A𝒫A𝒫AA×A
49 endom 𝒫AA×A𝒫AA×A
50 48 49 syl A×A𝒫A𝒫AA×A
51 47 50 nsyl AGCH¬AFin¬A×A𝒫A
52 brsdom A×A𝒫AA×A𝒫A¬A×A𝒫A
53 44 51 52 sylanbrc AGCH¬AFinA×A𝒫A
54 21 53 jca AGCH¬AFinAA×AA×A𝒫A
55 gchen1 AGCH¬AFinAA×AA×A𝒫AAA×A
56 54 55 mpdan AGCH¬AFinAA×A
57 56 ensymd AGCH¬AFinA×AA