Metamath Proof Explorer

Theorem gchhar

Description: A "local" form of gchac . If A and ~P A are GCH-sets, then the Hartogs number of A is ~P A (so ~P A and a fortiori A are well-orderable). The proof is due to Specker. Theorem 2.1 of KanamoriPincus p. 419. (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Assertion gchhar ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→har⁡A≈𝒫A

Proof

Step Hyp Ref Expression
1 harcl ⊢har⁡A∈On
2 simp3 ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A∈GCH
3 djudoml ⊢har⁡A∈On∧𝒫A∈GCH→har⁡A≼har⁡A⊔︀𝒫A
4 1 2 3 sylancr ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→har⁡A≼har⁡A⊔︀𝒫A
5 domnsym ⊢ω≼A→¬A≺ω
6 5 3ad2ant1 ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→¬A≺ω
7 isfinite ⊢A∈Fin↔A≺ω
8 6 7 sylnibr ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→¬A∈Fin
9 pwfi ⊢A∈Fin↔𝒫A∈Fin
10 8 9 sylnib ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→¬𝒫A∈Fin
11 djudoml ⊢𝒫A∈GCH∧har⁡A∈On→𝒫A≼𝒫A⊔︀har⁡A
12 2 1 11 sylancl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A≼𝒫A⊔︀har⁡A
13 fvexd ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→har⁡A∈V
14 djuex ⊢𝒫A∈GCH∧har⁡A∈V→𝒫A⊔︀har⁡A∈V
15 2 13 14 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A⊔︀har⁡A∈V
16 canth2g ⊢𝒫A⊔︀har⁡A∈V→𝒫A⊔︀har⁡A≺𝒫𝒫A⊔︀har⁡A
17 15 16 syl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A⊔︀har⁡A≺𝒫𝒫A⊔︀har⁡A
18 pwdjuen ⊢𝒫A∈GCH∧har⁡A∈On→𝒫𝒫A⊔︀har⁡A≈𝒫𝒫A×𝒫har⁡A
19 2 1 18 sylancl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫𝒫A⊔︀har⁡A≈𝒫𝒫A×𝒫har⁡A
20 2 pwexd ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫𝒫A∈V
21 simp2 ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A∈GCH
22 harwdom ⊢A∈GCH→har⁡A≼*𝒫A×A
23 wdompwdom ⊢har⁡A≼*𝒫A×A→𝒫har⁡A≼𝒫𝒫A×A
24 21 22 23 3syl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫har⁡A≼𝒫𝒫A×A
25 xpdom2g ⊢𝒫𝒫A∈V∧𝒫har⁡A≼𝒫𝒫A×A→𝒫𝒫A×𝒫har⁡A≼𝒫𝒫A×𝒫𝒫A×A
26 20 24 25 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫𝒫A×𝒫har⁡A≼𝒫𝒫A×𝒫𝒫A×A
27 21 21 xpexd ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A×A∈V
28 27 pwexd ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A×A∈V
29 pwdjuen ⊢𝒫A∈GCH∧𝒫A×A∈V→𝒫𝒫A⊔︀𝒫A×A≈𝒫𝒫A×𝒫𝒫A×A
30 2 28 29 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫𝒫A⊔︀𝒫A×A≈𝒫𝒫A×𝒫𝒫A×A
31 30 ensymd ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫𝒫A×𝒫𝒫A×A≈𝒫𝒫A⊔︀𝒫A×A
32 enrefg ⊢𝒫A∈GCH→𝒫A≈𝒫A
33 2 32 syl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A≈𝒫A
34 gchxpidm ⊢A∈GCH∧¬A∈Fin→A×A≈A
35 21 8 34 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A×A≈A
36 pwen ⊢A×A≈A→𝒫A×A≈𝒫A
37 35 36 syl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A×A≈𝒫A
38 djuen ⊢𝒫A≈𝒫A∧𝒫A×A≈𝒫A→𝒫A⊔︀𝒫A×A≈𝒫A⊔︀𝒫A
39 33 37 38 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A⊔︀𝒫A×A≈𝒫A⊔︀𝒫A
40 gchdjuidm ⊢𝒫A∈GCH∧¬𝒫A∈Fin→𝒫A⊔︀𝒫A≈𝒫A
41 2 10 40 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A⊔︀𝒫A≈𝒫A
42 entr ⊢𝒫A⊔︀𝒫A×A≈𝒫A⊔︀𝒫A∧𝒫A⊔︀𝒫A≈𝒫A→𝒫A⊔︀𝒫A×A≈𝒫A
43 39 41 42 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A⊔︀𝒫A×A≈𝒫A
44 pwen ⊢𝒫A⊔︀𝒫A×A≈𝒫A→𝒫𝒫A⊔︀𝒫A×A≈𝒫𝒫A
45 43 44 syl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫𝒫A⊔︀𝒫A×A≈𝒫𝒫A
46 entr ⊢𝒫𝒫A×𝒫𝒫A×A≈𝒫𝒫A⊔︀𝒫A×A∧𝒫𝒫A⊔︀𝒫A×A≈𝒫𝒫A→𝒫𝒫A×𝒫𝒫A×A≈𝒫𝒫A
47 31 45 46 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫𝒫A×𝒫𝒫A×A≈𝒫𝒫A
48 domentr ⊢𝒫𝒫A×𝒫har⁡A≼𝒫𝒫A×𝒫𝒫A×A∧𝒫𝒫A×𝒫𝒫A×A≈𝒫𝒫A→𝒫𝒫A×𝒫har⁡A≼𝒫𝒫A
49 26 47 48 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫𝒫A×𝒫har⁡A≼𝒫𝒫A
50 endomtr ⊢𝒫𝒫A⊔︀har⁡A≈𝒫𝒫A×𝒫har⁡A∧𝒫𝒫A×𝒫har⁡A≼𝒫𝒫A→𝒫𝒫A⊔︀har⁡A≼𝒫𝒫A
51 19 49 50 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫𝒫A⊔︀har⁡A≼𝒫𝒫A
52 sdomdomtr ⊢𝒫A⊔︀har⁡A≺𝒫𝒫A⊔︀har⁡A∧𝒫𝒫A⊔︀har⁡A≼𝒫𝒫A→𝒫A⊔︀har⁡A≺𝒫𝒫A
53 17 51 52 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A⊔︀har⁡A≺𝒫𝒫A
54 gchen1 ⊢𝒫A∈GCH∧¬𝒫A∈Fin∧𝒫A≼𝒫A⊔︀har⁡A∧𝒫A⊔︀har⁡A≺𝒫𝒫A→𝒫A≈𝒫A⊔︀har⁡A
55 2 10 12 53 54 syl22anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A≈𝒫A⊔︀har⁡A
56 djucomen ⊢𝒫A∈GCH∧har⁡A∈V→𝒫A⊔︀har⁡A≈har⁡A⊔︀𝒫A
57 2 13 56 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A⊔︀har⁡A≈har⁡A⊔︀𝒫A
58 entr ⊢𝒫A≈𝒫A⊔︀har⁡A∧𝒫A⊔︀har⁡A≈har⁡A⊔︀𝒫A→𝒫A≈har⁡A⊔︀𝒫A
59 55 57 58 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A≈har⁡A⊔︀𝒫A
60 59 ensymd ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→har⁡A⊔︀𝒫A≈𝒫A
61 domentr ⊢har⁡A≼har⁡A⊔︀𝒫A∧har⁡A⊔︀𝒫A≈𝒫A→har⁡A≼𝒫A
62 4 60 61 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→har⁡A≼𝒫A
63 gchdjuidm ⊢A∈GCH∧¬A∈Fin→A⊔︀A≈A
64 21 8 63 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A⊔︀A≈A
65 pwen ⊢A⊔︀A≈A→𝒫A⊔︀A≈𝒫A
66 64 65 syl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A⊔︀A≈𝒫A
67 djudoml ⊢A∈GCH∧har⁡A∈On→A≼A⊔︀har⁡A
68 21 1 67 sylancl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A≼A⊔︀har⁡A
69 harndom ⊢¬har⁡A≼A
70 djudoml ⊢har⁡A∈On∧A∈GCH→har⁡A≼har⁡A⊔︀A
71 1 21 70 sylancr ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→har⁡A≼har⁡A⊔︀A
72 djucomen ⊢har⁡A∈On∧A∈GCH→har⁡A⊔︀A≈A⊔︀har⁡A
73 1 21 72 sylancr ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→har⁡A⊔︀A≈A⊔︀har⁡A
74 domentr ⊢har⁡A≼har⁡A⊔︀A∧har⁡A⊔︀A≈A⊔︀har⁡A→har⁡A≼A⊔︀har⁡A
75 71 73 74 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→har⁡A≼A⊔︀har⁡A
76 domen2 ⊢A≈A⊔︀har⁡A→har⁡A≼A↔har⁡A≼A⊔︀har⁡A
77 75 76 syl5ibrcom ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A≈A⊔︀har⁡A→har⁡A≼A
78 69 77 mtoi ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→¬A≈A⊔︀har⁡A
79 brsdom ⊢A≺A⊔︀har⁡A↔A≼A⊔︀har⁡A∧¬A≈A⊔︀har⁡A
80 68 78 79 sylanbrc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A≺A⊔︀har⁡A
81 canth2g ⊢A∈GCH→A≺𝒫A
82 sdomdom ⊢A≺𝒫A→A≼𝒫A
83 21 81 82 3syl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A≼𝒫A
84 djudom1 ⊢A≼𝒫A∧har⁡A∈On→A⊔︀har⁡A≼𝒫A⊔︀har⁡A
85 83 1 84 sylancl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A⊔︀har⁡A≼𝒫A⊔︀har⁡A
86 djudom2 ⊢har⁡A≼𝒫A∧𝒫A∈GCH→𝒫A⊔︀har⁡A≼𝒫A⊔︀𝒫A
87 62 2 86 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A⊔︀har⁡A≼𝒫A⊔︀𝒫A
88 domtr ⊢A⊔︀har⁡A≼𝒫A⊔︀har⁡A∧𝒫A⊔︀har⁡A≼𝒫A⊔︀𝒫A→A⊔︀har⁡A≼𝒫A⊔︀𝒫A
89 85 87 88 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A⊔︀har⁡A≼𝒫A⊔︀𝒫A
90 domentr ⊢A⊔︀har⁡A≼𝒫A⊔︀𝒫A∧𝒫A⊔︀𝒫A≈𝒫A→A⊔︀har⁡A≼𝒫A
91 89 41 90 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A⊔︀har⁡A≼𝒫A
92 gchen2 ⊢A∈GCH∧¬A∈Fin∧A≺A⊔︀har⁡A∧A⊔︀har⁡A≼𝒫A→A⊔︀har⁡A≈𝒫A
93 21 8 80 91 92 syl22anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→A⊔︀har⁡A≈𝒫A
94 93 ensymd ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A≈A⊔︀har⁡A
95 entr ⊢𝒫A⊔︀A≈𝒫A∧𝒫A≈A⊔︀har⁡A→𝒫A⊔︀A≈A⊔︀har⁡A
96 66 94 95 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A⊔︀A≈A⊔︀har⁡A
97 endom ⊢𝒫A⊔︀A≈A⊔︀har⁡A→𝒫A⊔︀A≼A⊔︀har⁡A
98 pwdjudom ⊢𝒫A⊔︀A≼A⊔︀har⁡A→𝒫A≼har⁡A
99 96 97 98 3syl ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→𝒫A≼har⁡A
100 sbth ⊢har⁡A≼𝒫A∧𝒫A≼har⁡A→har⁡A≈𝒫A
101 62 99 100 syl2anc ⊢ω≼A∧A∈GCH∧𝒫A∈GCH→har⁡A≈𝒫A