Theorem gchhar 10748

Description: A "local" form of gchac 10750. 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 9628	. . . 4 ⊢ (har‘𝐴) ∈ On
2		simp3 1138	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ∈ GCH)
3		djudoml 10254	. . . 4 ⊢ (((har‘𝐴) ∈ On ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝒫 𝐴))
4	1, 2, 3	sylancr 586	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝒫 𝐴))
5		domnsym 9165	. . . . . . . . 9 ⊢ (ω ≼ 𝐴 → ¬ 𝐴 ≺ ω)
6	5	3ad2ant1 1133	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ≺ ω)
7		isfinite 9721	. . . . . . . 8 ⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺ ω)
8	6, 7	sylnibr 329	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ∈ Fin)
9		pwfi 9385	. . . . . . 7 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
10	8, 9	sylnib 328	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝒫 𝐴 ∈ Fin)
11		djudoml 10254	. . . . . . 7 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
12	2, 1, 11	sylancl 585	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
13		fvexd 6935	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ∈ V)
14		djuex 9977	. . . . . . . . 9 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ V) → (𝒫 𝐴 ⊔ (har‘𝐴)) ∈ V)
15	2, 13, 14	syl2anc 583	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ∈ V)
16		canth2g 9197	. . . . . . . 8 ⊢ ((𝒫 𝐴 ⊔ (har‘𝐴)) ∈ V → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)))
17	15, 16	syl 17	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)))
18		pwdjuen 10251	. . . . . . . . 9 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)))
19	2, 1, 18	sylancl 585	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)))
20	2	pwexd 5397	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝒫 𝐴 ∈ V)
21		simp2 1137	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ∈ GCH)
22		harwdom 9660	. . . . . . . . . . 11 ⊢ (𝐴 ∈ GCH → (har‘𝐴) ≼* 𝒫 (𝐴 × 𝐴))
23		wdompwdom 9647	. . . . . . . . . . 11 ⊢ ((har‘𝐴) ≼* 𝒫 (𝐴 × 𝐴) → 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴))
24	21, 22, 23	3syl 18	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴))
25		xpdom2g 9134	. . . . . . . . . 10 ⊢ ((𝒫 𝒫 𝐴 ∈ V ∧ 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴)) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
26	20, 24, 25	syl2anc 583	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
27	21, 21	xpexd 7786	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 × 𝐴) ∈ V)
28	27	pwexd 5397	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 × 𝐴) ∈ V)
29		pwdjuen 10251	. . . . . . . . . . . 12 ⊢ ((𝒫 𝐴 ∈ GCH ∧ 𝒫 (𝐴 × 𝐴) ∈ V) → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
30	2, 28, 29	syl2anc 583	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
31	30	ensymd 9065	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)))
32		enrefg 9044	. . . . . . . . . . . . . 14 ⊢ (𝒫 𝐴 ∈ GCH → 𝒫 𝐴 ≈ 𝒫 𝐴)
33	2, 32	syl 17	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ 𝒫 𝐴)
34		gchxpidm 10738	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴)
35	21, 8, 34	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 × 𝐴) ≈ 𝐴)
36		pwen 9216	. . . . . . . . . . . . . 14 ⊢ ((𝐴 × 𝐴) ≈ 𝐴 → 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴)
37	35, 36	syl 17	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴)
38		djuen 10239	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝐴 ≈ 𝒫 𝐴 ∧ 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
39	33, 37, 38	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
40		gchdjuidm 10737	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝐴 ∈ GCH ∧ ¬ 𝒫 𝐴 ∈ Fin) → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
41	2, 10, 40	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
42		entr 9066	. . . . . . . . . . . 12 ⊢ (((𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴) ∧ (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴)
43	39, 41, 42	syl2anc 583	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴)
44		pwen 9216	. . . . . . . . . . 11 ⊢ ((𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴 → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
45	43, 44	syl 17	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
46		entr 9066	. . . . . . . . . 10 ⊢ (((𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ∧ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
47	31, 45, 46	syl2anc 583	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
48		domentr 9073	. . . . . . . . 9 ⊢ (((𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
49	26, 47, 48	syl2anc 583	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
50		endomtr 9072	. . . . . . . 8 ⊢ ((𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ∧ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
51	19, 49, 50	syl2anc 583	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
52		sdomdomtr 9176	. . . . . . 7 ⊢ (((𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)
53	17, 51, 52	syl2anc 583	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)
54		gchen1 10694	. . . . . 6 ⊢ (((𝒫 𝐴 ∈ GCH ∧ ¬ 𝒫 𝐴 ∈ Fin) ∧ (𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)) → 𝒫 𝐴 ≈ (𝒫 𝐴 ⊔ (har‘𝐴)))
55	2, 10, 12, 53, 54	syl22anc 838	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ (𝒫 𝐴 ⊔ (har‘𝐴)))
56		djucomen 10247	. . . . . 6 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ V) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
57	2, 13, 56	syl2anc 583	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
58		entr 9066	. . . . 5 ⊢ ((𝒫 𝐴 ≈ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ ((har‘𝐴) ⊔ 𝒫 𝐴)) → 𝒫 𝐴 ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
59	55, 57, 58	syl2anc 583	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
60	59	ensymd 9065	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ((har‘𝐴) ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
61		domentr 9073	. . 3 ⊢ (((har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝒫 𝐴) ∧ ((har‘𝐴) ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) → (har‘𝐴) ≼ 𝒫 𝐴)
62	4, 60, 61	syl2anc 583	. 2 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ 𝒫 𝐴)
63		gchdjuidm 10737	. . . . . 6 ⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 𝐴) ≈ 𝐴)
64	21, 8, 63	syl2anc 583	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ 𝐴) ≈ 𝐴)
65		pwen 9216	. . . . 5 ⊢ ((𝐴 ⊔ 𝐴) ≈ 𝐴 → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴)
66	64, 65	syl 17	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴)
67		djudoml 10254	. . . . . . . 8 ⊢ ((𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝐴 ≼ (𝐴 ⊔ (har‘𝐴)))
68	21, 1, 67	sylancl 585	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≼ (𝐴 ⊔ (har‘𝐴)))
69		harndom 9631	. . . . . . . 8 ⊢ ¬ (har‘𝐴) ≼ 𝐴
70		djudoml 10254	. . . . . . . . . . 11 ⊢ (((har‘𝐴) ∈ On ∧ 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝐴))
71	1, 21, 70	sylancr 586	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝐴))
72		djucomen 10247	. . . . . . . . . . 11 ⊢ (((har‘𝐴) ∈ On ∧ 𝐴 ∈ GCH) → ((har‘𝐴) ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
73	1, 21, 72	sylancr 586	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ((har‘𝐴) ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
74		domentr 9073	. . . . . . . . . 10 ⊢ (((har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝐴) ∧ ((har‘𝐴) ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴))) → (har‘𝐴) ≼ (𝐴 ⊔ (har‘𝐴)))
75	71, 73, 74	syl2anc 583	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ (𝐴 ⊔ (har‘𝐴)))
76		domen2 9186	. . . . . . . . 9 ⊢ (𝐴 ≈ (𝐴 ⊔ (har‘𝐴)) → ((har‘𝐴) ≼ 𝐴 ↔ (har‘𝐴) ≼ (𝐴 ⊔ (har‘𝐴))))
77	75, 76	syl5ibrcom 247	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ≈ (𝐴 ⊔ (har‘𝐴)) → (har‘𝐴) ≼ 𝐴))
78	69, 77	mtoi 199	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ≈ (𝐴 ⊔ (har‘𝐴)))
79		brsdom 9035	. . . . . . 7 ⊢ (𝐴 ≺ (𝐴 ⊔ (har‘𝐴)) ↔ (𝐴 ≼ (𝐴 ⊔ (har‘𝐴)) ∧ ¬ 𝐴 ≈ (𝐴 ⊔ (har‘𝐴))))
80	68, 78, 79	sylanbrc 582	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≺ (𝐴 ⊔ (har‘𝐴)))
81		canth2g 9197	. . . . . . . . . 10 ⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴)
82		sdomdom 9040	. . . . . . . . . 10 ⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴)
83	21, 81, 82	3syl 18	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≼ 𝒫 𝐴)
84		djudom1 10252	. . . . . . . . 9 ⊢ ((𝐴 ≼ 𝒫 𝐴 ∧ (har‘𝐴) ∈ On) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
85	83, 1, 84	sylancl 585	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
86		djudom2 10253	. . . . . . . . 9 ⊢ (((har‘𝐴) ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
87	62, 2, 86	syl2anc 583	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
88		domtr 9067	. . . . . . . 8 ⊢ (((𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴)) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
89	85, 87, 88	syl2anc 583	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
90		domentr 9073	. . . . . . 7 ⊢ (((𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴) ∧ (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴)
91	89, 41, 90	syl2anc 583	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴)
92		gchen2 10695	. . . . . 6 ⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ (𝐴 ⊔ (har‘𝐴)) ∧ (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴)) → (𝐴 ⊔ (har‘𝐴)) ≈ 𝒫 𝐴)
93	21, 8, 80, 91, 92	syl22anc 838	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≈ 𝒫 𝐴)
94	93	ensymd 9065	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ (𝐴 ⊔ (har‘𝐴)))
95		entr 9066	. . . 4 ⊢ ((𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴 ∧ 𝒫 𝐴 ≈ (𝐴 ⊔ (har‘𝐴))) → 𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
96	66, 94, 95	syl2anc 583	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
97		endom 9039	. . 3 ⊢ (𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)) → 𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ (har‘𝐴)))
98		pwdjudom 10284	. . 3 ⊢ (𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ (har‘𝐴)) → 𝒫 𝐴 ≼ (har‘𝐴))
99	96, 97, 98	3syl 18	. 2 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≼ (har‘𝐴))
100		sbth 9159	. 2 ⊢ (((har‘𝐴) ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ (har‘𝐴)) → (har‘𝐴) ≈ 𝒫 𝐴)
101	62, 99, 100	syl2anc 583	1 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≈ 𝒫 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ w3a 1087   ∈ wcel 2108  Vcvv 3488  𝒫 cpw 4622   class class class wbr 5166   × cxp 5698  Oncon0 6395  ‘cfv 6573  ωcom 7903   ≈ cen 9000   ≼ cdom 9001   ≺ csdm 9002  Fincfn 9003  harchar 9625   ≼^* cwdom 9633   ⊔ cdju 9967  GCHcgch 10689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-seqom 8504  df-1o 8522  df-2o 8523  df-oadd 8526  df-omul 8527  df-oexp 8528  df-er 8763  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-oi 9579  df-har 9626  df-wdom 9634  df-cnf 9731  df-dju 9970  df-card 10008  df-fin4 10356  df-gch 10690

This theorem is referenced by:  gchacg  10749