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 ( ( ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH ) → ( har ‘ 𝐴 ) ≈ 𝒫 𝐴 )

Proof

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