Theorem gchhar 9783

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

Assertion

Ref	Expression
gchhar	⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≈ 𝒫 𝐴)

Proof of Theorem gchhar

Step	Hyp	Ref	Expression
1		harcl 8702	. . . 4 ⊢ (har‘𝐴) ∈ On
2		simp3 1161	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ∈ GCH)
3		cdadom3 9292	. . . 4 ⊢ (((har‘𝐴) ∈ On ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) +𝑐 𝒫 𝐴))
4	1, 2, 3	sylancr 577	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) +𝑐 𝒫 𝐴))
5		domnsym 8322	. . . . . . . . 9 ⊢ (ω ≼ 𝐴 → ¬ 𝐴 ≺ ω)
6	5	3ad2ant1 1156	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ≺ ω)
7		isfinite 8793	. . . . . . . 8 ⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺ ω)
8	6, 7	sylnibr 320	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ∈ Fin)
9		pwfi 8497	. . . . . . 7 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
10	8, 9	sylnib 319	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝒫 𝐴 ∈ Fin)
11		cdadom3 9292	. . . . . . 7 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝒫 𝐴 ≼ (𝒫 𝐴 +𝑐 (har‘𝐴)))
12	2, 1, 11	sylancl 576	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≼ (𝒫 𝐴 +𝑐 (har‘𝐴)))
13		ovex 6903	. . . . . . . 8 ⊢ (𝒫 𝐴 +𝑐 (har‘𝐴)) ∈ V
14	13	canth2 8349	. . . . . . 7 ⊢ (𝒫 𝐴 +𝑐 (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 +𝑐 (har‘𝐴))
15		pwcdaen 9289	. . . . . . . . 9 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝒫 (𝒫 𝐴 +𝑐 (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)))
16	2, 1, 15	sylancl 576	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 +𝑐 (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)))
17	2	pwexd 5046	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝒫 𝐴 ∈ V)
18		simp2 1160	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ∈ GCH)
19		harwdom 8731	. . . . . . . . . . 11 ⊢ (𝐴 ∈ GCH → (har‘𝐴) ≼* 𝒫 (𝐴 × 𝐴))
20		wdompwdom 8719	. . . . . . . . . . 11 ⊢ ((har‘𝐴) ≼* 𝒫 (𝐴 × 𝐴) → 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴))
21	18, 19, 20	3syl 18	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴))
22		xpdom2g 8292	. . . . . . . . . 10 ⊢ ((𝒫 𝒫 𝐴 ∈ V ∧ 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴)) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
23	17, 21, 22	syl2anc 575	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
24		xpexg 7187	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ GCH ∧ 𝐴 ∈ GCH) → (𝐴 × 𝐴) ∈ V)
25	18, 18, 24	syl2anc 575	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 × 𝐴) ∈ V)
26	25	pwexd 5046	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 × 𝐴) ∈ V)
27		pwcdaen 9289	. . . . . . . . . . . 12 ⊢ ((𝒫 𝐴 ∈ GCH ∧ 𝒫 (𝐴 × 𝐴) ∈ V) → 𝒫 (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
28	2, 26, 27	syl2anc 575	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
29	28	ensymd 8240	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)))
30		enrefg 8221	. . . . . . . . . . . . . 14 ⊢ (𝒫 𝐴 ∈ GCH → 𝒫 𝐴 ≈ 𝒫 𝐴)
31	2, 30	syl 17	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ 𝒫 𝐴)
32		gchxpidm 9773	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴)
33	18, 8, 32	syl2anc 575	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 × 𝐴) ≈ 𝐴)
34		pwen 8369	. . . . . . . . . . . . . 14 ⊢ ((𝐴 × 𝐴) ≈ 𝐴 → 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴)
35	33, 34	syl 17	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴)
36		cdaen 9277	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝐴 ≈ 𝒫 𝐴 ∧ 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 +𝑐 𝒫 𝐴))
37	31, 35, 36	syl2anc 575	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 +𝑐 𝒫 𝐴))
38		gchcdaidm 9772	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝐴 ∈ GCH ∧ ¬ 𝒫 𝐴 ∈ Fin) → (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴)
39	2, 10, 38	syl2anc 575	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴)
40		entr 8241	. . . . . . . . . . . 12 ⊢ (((𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 +𝑐 𝒫 𝐴) ∧ (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴)
41	37, 39, 40	syl2anc 575	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴)
42		pwen 8369	. . . . . . . . . . 11 ⊢ ((𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴 → 𝒫 (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
43	41, 42	syl 17	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
44		entr 8241	. . . . . . . . . 10 ⊢ (((𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ∧ 𝒫 (𝒫 𝐴 +𝑐 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
45	29, 43, 44	syl2anc 575	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
46		domentr 8248	. . . . . . . . 9 ⊢ (((𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
47	23, 45, 46	syl2anc 575	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
48		endomtr 8247	. . . . . . . 8 ⊢ ((𝒫 (𝒫 𝐴 +𝑐 (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ∧ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → 𝒫 (𝒫 𝐴 +𝑐 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
49	16, 47, 48	syl2anc 575	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 +𝑐 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
50		sdomdomtr 8329	. . . . . . 7 ⊢ (((𝒫 𝐴 +𝑐 (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 +𝑐 (har‘𝐴)) ∧ 𝒫 (𝒫 𝐴 +𝑐 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → (𝒫 𝐴 +𝑐 (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)
51	14, 49, 50	sylancr 577	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 +𝑐 (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)
52		gchen1 9729	. . . . . 6 ⊢ (((𝒫 𝐴 ∈ GCH ∧ ¬ 𝒫 𝐴 ∈ Fin) ∧ (𝒫 𝐴 ≼ (𝒫 𝐴 +𝑐 (har‘𝐴)) ∧ (𝒫 𝐴 +𝑐 (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)) → 𝒫 𝐴 ≈ (𝒫 𝐴 +𝑐 (har‘𝐴)))
53	2, 10, 12, 51, 52	syl22anc 858	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ (𝒫 𝐴 +𝑐 (har‘𝐴)))
54		cdacomen 9285	. . . . 5 ⊢ (𝒫 𝐴 +𝑐 (har‘𝐴)) ≈ ((har‘𝐴) +𝑐 𝒫 𝐴)
55		entr 8241	. . . . 5 ⊢ ((𝒫 𝐴 ≈ (𝒫 𝐴 +𝑐 (har‘𝐴)) ∧ (𝒫 𝐴 +𝑐 (har‘𝐴)) ≈ ((har‘𝐴) +𝑐 𝒫 𝐴)) → 𝒫 𝐴 ≈ ((har‘𝐴) +𝑐 𝒫 𝐴))
56	53, 54, 55	sylancl 576	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ ((har‘𝐴) +𝑐 𝒫 𝐴))
57	56	ensymd 8240	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ((har‘𝐴) +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴)
58		domentr 8248	. . 3 ⊢ (((har‘𝐴) ≼ ((har‘𝐴) +𝑐 𝒫 𝐴) ∧ ((har‘𝐴) +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) → (har‘𝐴) ≼ 𝒫 𝐴)
59	4, 57, 58	syl2anc 575	. 2 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ 𝒫 𝐴)
60		gchcdaidm 9772	. . . . . 6 ⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 𝐴) ≈ 𝐴)
61	18, 8, 60	syl2anc 575	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 +𝑐 𝐴) ≈ 𝐴)
62		pwen 8369	. . . . 5 ⊢ ((𝐴 +𝑐 𝐴) ≈ 𝐴 → 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴)
63	61, 62	syl 17	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴)
64		cdadom3 9292	. . . . . . . 8 ⊢ ((𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝐴 ≼ (𝐴 +𝑐 (har‘𝐴)))
65	18, 1, 64	sylancl 576	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≼ (𝐴 +𝑐 (har‘𝐴)))
66		harndom 8705	. . . . . . . 8 ⊢ ¬ (har‘𝐴) ≼ 𝐴
67		cdadom3 9292	. . . . . . . . . . 11 ⊢ (((har‘𝐴) ∈ On ∧ 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) +𝑐 𝐴))
68	1, 18, 67	sylancr 577	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) +𝑐 𝐴))
69		cdacomen 9285	. . . . . . . . . 10 ⊢ ((har‘𝐴) +𝑐 𝐴) ≈ (𝐴 +𝑐 (har‘𝐴))
70		domentr 8248	. . . . . . . . . 10 ⊢ (((har‘𝐴) ≼ ((har‘𝐴) +𝑐 𝐴) ∧ ((har‘𝐴) +𝑐 𝐴) ≈ (𝐴 +𝑐 (har‘𝐴))) → (har‘𝐴) ≼ (𝐴 +𝑐 (har‘𝐴)))
71	68, 69, 70	sylancl 576	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ (𝐴 +𝑐 (har‘𝐴)))
72		domen2 8339	. . . . . . . . 9 ⊢ (𝐴 ≈ (𝐴 +𝑐 (har‘𝐴)) → ((har‘𝐴) ≼ 𝐴 ↔ (har‘𝐴) ≼ (𝐴 +𝑐 (har‘𝐴))))
73	71, 72	syl5ibrcom 238	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ≈ (𝐴 +𝑐 (har‘𝐴)) → (har‘𝐴) ≼ 𝐴))
74	66, 73	mtoi 190	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ≈ (𝐴 +𝑐 (har‘𝐴)))
75		brsdom 8212	. . . . . . 7 ⊢ (𝐴 ≺ (𝐴 +𝑐 (har‘𝐴)) ↔ (𝐴 ≼ (𝐴 +𝑐 (har‘𝐴)) ∧ ¬ 𝐴 ≈ (𝐴 +𝑐 (har‘𝐴))))
76	65, 74, 75	sylanbrc 574	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≺ (𝐴 +𝑐 (har‘𝐴)))
77		canth2g 8350	. . . . . . . . 9 ⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴)
78		sdomdom 8217	. . . . . . . . 9 ⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴)
79		cdadom1 9290	. . . . . . . . 9 ⊢ (𝐴 ≼ 𝒫 𝐴 → (𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 (har‘𝐴)))
80	18, 77, 78, 79	4syl 19	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 (har‘𝐴)))
81		cdadom2 9291	. . . . . . . . 9 ⊢ ((har‘𝐴) ≼ 𝒫 𝐴 → (𝒫 𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴))
82	59, 81	syl 17	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴))
83		domtr 8242	. . . . . . . 8 ⊢ (((𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 (har‘𝐴)) ∧ (𝒫 𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴)) → (𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴))
84	80, 82, 83	syl2anc 575	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴))
85		domentr 8248	. . . . . . 7 ⊢ (((𝐴 +𝑐 (har‘𝐴)) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴) ∧ (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝐴 +𝑐 (har‘𝐴)) ≼ 𝒫 𝐴)
86	84, 39, 85	syl2anc 575	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 +𝑐 (har‘𝐴)) ≼ 𝒫 𝐴)
87		gchen2 9730	. . . . . 6 ⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ (𝐴 +𝑐 (har‘𝐴)) ∧ (𝐴 +𝑐 (har‘𝐴)) ≼ 𝒫 𝐴)) → (𝐴 +𝑐 (har‘𝐴)) ≈ 𝒫 𝐴)
88	18, 8, 76, 86, 87	syl22anc 858	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 +𝑐 (har‘𝐴)) ≈ 𝒫 𝐴)
89	88	ensymd 8240	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ (𝐴 +𝑐 (har‘𝐴)))
90		entr 8241	. . . 4 ⊢ ((𝒫 (𝐴 +𝑐 𝐴) ≈ 𝒫 𝐴 ∧ 𝒫 𝐴 ≈ (𝐴 +𝑐 (har‘𝐴))) → 𝒫 (𝐴 +𝑐 𝐴) ≈ (𝐴 +𝑐 (har‘𝐴)))
91	63, 89, 90	syl2anc 575	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 +𝑐 𝐴) ≈ (𝐴 +𝑐 (har‘𝐴)))
92		endom 8216	. . 3 ⊢ (𝒫 (𝐴 +𝑐 𝐴) ≈ (𝐴 +𝑐 (har‘𝐴)) → 𝒫 (𝐴 +𝑐 𝐴) ≼ (𝐴 +𝑐 (har‘𝐴)))
93		pwcdadom 9320	. . 3 ⊢ (𝒫 (𝐴 +𝑐 𝐴) ≼ (𝐴 +𝑐 (har‘𝐴)) → 𝒫 𝐴 ≼ (har‘𝐴))
94	91, 92, 93	3syl 18	. 2 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≼ (har‘𝐴))
95		sbth 8316	. 2 ⊢ (((har‘𝐴) ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ (har‘𝐴)) → (har‘𝐴) ≈ 𝒫 𝐴)
96	59, 94, 95	syl2anc 575	1 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≈ 𝒫 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ w3a 1100   ∈ wcel 2158  Vcvv 3390  𝒫 cpw 4348   class class class wbr 4840   × cxp 5306  Oncon0 5933  ‘cfv 6098  (class class class)co 6871  ωcom 7292   ≈ cen 8186   ≼ cdom 8187   ≺ csdm 8188  Fincfn 8189  harchar 8697   ≼^* cwdom 8698   +_𝑐 ccda 9271  GCHcgch 9724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-inf2 8782

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-se 5268  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-isom 6107  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-om 7293  df-1st 7395  df-2nd 7396  df-supp 7527  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-seqom 7776  df-1o 7793  df-2o 7794  df-oadd 7797  df-omul 7798  df-oexp 7799  df-er 7976  df-map 8091  df-en 8190  df-dom 8191  df-sdom 8192  df-fin 8193  df-fsupp 8512  df-oi 8651  df-har 8699  df-wdom 8700  df-cnf 8803  df-card 9045  df-cda 9272  df-fin4 9391  df-gch 9725

This theorem is referenced by:  gchacg  9784