Theorem gchhar 10602

Description: A "local" form of gchac 10604. 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 9474	. . . 4 ⊢ (har‘𝐴) ∈ On
2		simp3 1139	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ∈ GCH)
3		djudoml 10107	. . . 4 ⊢ (((har‘𝐴) ∈ On ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝒫 𝐴))
4	1, 2, 3	sylancr 588	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝒫 𝐴))
5		domnsym 9041	. . . . . . . . 9 ⊢ (ω ≼ 𝐴 → ¬ 𝐴 ≺ ω)
6	5	3ad2ant1 1134	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ≺ ω)
7		isfinite 9573	. . . . . . . 8 ⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺ ω)
8	6, 7	sylnibr 329	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ∈ Fin)
9		pwfi 9229	. . . . . . 7 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
10	8, 9	sylnib 328	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝒫 𝐴 ∈ Fin)
11		djudoml 10107	. . . . . . 7 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
12	2, 1, 11	sylancl 587	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
13		fvexd 6855	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ∈ V)
14		djuex 9832	. . . . . . . . 9 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ V) → (𝒫 𝐴 ⊔ (har‘𝐴)) ∈ V)
15	2, 13, 14	syl2anc 585	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ∈ V)
16		canth2g 9069	. . . . . . . 8 ⊢ ((𝒫 𝐴 ⊔ (har‘𝐴)) ∈ V → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)))
17	15, 16	syl 17	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)))
18		pwdjuen 10104	. . . . . . . . 9 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)))
19	2, 1, 18	sylancl 587	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)))
20	2	pwexd 5321	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝒫 𝐴 ∈ V)
21		simp2 1138	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ∈ GCH)
22		harwdom 9506	. . . . . . . . . . 11 ⊢ (𝐴 ∈ GCH → (har‘𝐴) ≼* 𝒫 (𝐴 × 𝐴))
23		wdompwdom 9493	. . . . . . . . . . 11 ⊢ ((har‘𝐴) ≼* 𝒫 (𝐴 × 𝐴) → 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴))
24	21, 22, 23	3syl 18	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴))
25		xpdom2g 9011	. . . . . . . . . 10 ⊢ ((𝒫 𝒫 𝐴 ∈ V ∧ 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴)) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
26	20, 24, 25	syl2anc 585	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
27	21, 21	xpexd 7705	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 × 𝐴) ∈ V)
28	27	pwexd 5321	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 × 𝐴) ∈ V)
29		pwdjuen 10104	. . . . . . . . . . . 12 ⊢ ((𝒫 𝐴 ∈ GCH ∧ 𝒫 (𝐴 × 𝐴) ∈ V) → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
30	2, 28, 29	syl2anc 585	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
31	30	ensymd 8952	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)))
32		enrefg 8931	. . . . . . . . . . . . . 14 ⊢ (𝒫 𝐴 ∈ GCH → 𝒫 𝐴 ≈ 𝒫 𝐴)
33	2, 32	syl 17	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ 𝒫 𝐴)
34		gchxpidm 10592	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴)
35	21, 8, 34	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 × 𝐴) ≈ 𝐴)
36		pwen 9088	. . . . . . . . . . . . . 14 ⊢ ((𝐴 × 𝐴) ≈ 𝐴 → 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴)
37	35, 36	syl 17	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴)
38		djuen 10092	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝐴 ≈ 𝒫 𝐴 ∧ 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
39	33, 37, 38	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
40		gchdjuidm 10591	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝐴 ∈ GCH ∧ ¬ 𝒫 𝐴 ∈ Fin) → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
41	2, 10, 40	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
42		entr 8953	. . . . . . . . . . . 12 ⊢ (((𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴) ∧ (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴)
43	39, 41, 42	syl2anc 585	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴)
44		pwen 9088	. . . . . . . . . . 11 ⊢ ((𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴 → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
45	43, 44	syl 17	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
46		entr 8953	. . . . . . . . . 10 ⊢ (((𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ∧ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
47	31, 45, 46	syl2anc 585	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
48		domentr 8960	. . . . . . . . 9 ⊢ (((𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
49	26, 47, 48	syl2anc 585	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
50		endomtr 8959	. . . . . . . 8 ⊢ ((𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ∧ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
51	19, 49, 50	syl2anc 585	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
52		sdomdomtr 9048	. . . . . . 7 ⊢ (((𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)
53	17, 51, 52	syl2anc 585	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)
54		gchen1 10548	. . . . . 6 ⊢ (((𝒫 𝐴 ∈ GCH ∧ ¬ 𝒫 𝐴 ∈ Fin) ∧ (𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)) → 𝒫 𝐴 ≈ (𝒫 𝐴 ⊔ (har‘𝐴)))
55	2, 10, 12, 53, 54	syl22anc 839	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ (𝒫 𝐴 ⊔ (har‘𝐴)))
56		djucomen 10100	. . . . . 6 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ V) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
57	2, 13, 56	syl2anc 585	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
58		entr 8953	. . . . 5 ⊢ ((𝒫 𝐴 ≈ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ ((har‘𝐴) ⊔ 𝒫 𝐴)) → 𝒫 𝐴 ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
59	55, 57, 58	syl2anc 585	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
60	59	ensymd 8952	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ((har‘𝐴) ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
61		domentr 8960	. . 3 ⊢ (((har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝒫 𝐴) ∧ ((har‘𝐴) ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) → (har‘𝐴) ≼ 𝒫 𝐴)
62	4, 60, 61	syl2anc 585	. 2 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ 𝒫 𝐴)
63		gchdjuidm 10591	. . . . . 6 ⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 𝐴) ≈ 𝐴)
64	21, 8, 63	syl2anc 585	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ 𝐴) ≈ 𝐴)
65		pwen 9088	. . . . 5 ⊢ ((𝐴 ⊔ 𝐴) ≈ 𝐴 → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴)
66	64, 65	syl 17	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴)
67		djudoml 10107	. . . . . . . 8 ⊢ ((𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝐴 ≼ (𝐴 ⊔ (har‘𝐴)))
68	21, 1, 67	sylancl 587	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≼ (𝐴 ⊔ (har‘𝐴)))
69		harndom 9477	. . . . . . . 8 ⊢ ¬ (har‘𝐴) ≼ 𝐴
70		djudoml 10107	. . . . . . . . . . 11 ⊢ (((har‘𝐴) ∈ On ∧ 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝐴))
71	1, 21, 70	sylancr 588	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝐴))
72		djucomen 10100	. . . . . . . . . . 11 ⊢ (((har‘𝐴) ∈ On ∧ 𝐴 ∈ GCH) → ((har‘𝐴) ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
73	1, 21, 72	sylancr 588	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ((har‘𝐴) ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
74		domentr 8960	. . . . . . . . . 10 ⊢ (((har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝐴) ∧ ((har‘𝐴) ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴))) → (har‘𝐴) ≼ (𝐴 ⊔ (har‘𝐴)))
75	71, 73, 74	syl2anc 585	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ (𝐴 ⊔ (har‘𝐴)))
76		domen2 9058	. . . . . . . . 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 8921	. . . . . . 7 ⊢ (𝐴 ≺ (𝐴 ⊔ (har‘𝐴)) ↔ (𝐴 ≼ (𝐴 ⊔ (har‘𝐴)) ∧ ¬ 𝐴 ≈ (𝐴 ⊔ (har‘𝐴))))
80	68, 78, 79	sylanbrc 584	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≺ (𝐴 ⊔ (har‘𝐴)))
81		canth2g 9069	. . . . . . . . . 10 ⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴)
82		sdomdom 8927	. . . . . . . . . 10 ⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴)
83	21, 81, 82	3syl 18	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≼ 𝒫 𝐴)
84		djudom1 10105	. . . . . . . . 9 ⊢ ((𝐴 ≼ 𝒫 𝐴 ∧ (har‘𝐴) ∈ On) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
85	83, 1, 84	sylancl 587	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
86		djudom2 10106	. . . . . . . . 9 ⊢ (((har‘𝐴) ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
87	62, 2, 86	syl2anc 585	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
88		domtr 8954	. . . . . . . 8 ⊢ (((𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴)) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
89	85, 87, 88	syl2anc 585	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
90		domentr 8960	. . . . . . 7 ⊢ (((𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴) ∧ (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴)
91	89, 41, 90	syl2anc 585	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴)
92		gchen2 10549	. . . . . 6 ⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ (𝐴 ⊔ (har‘𝐴)) ∧ (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴)) → (𝐴 ⊔ (har‘𝐴)) ≈ 𝒫 𝐴)
93	21, 8, 80, 91, 92	syl22anc 839	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≈ 𝒫 𝐴)
94	93	ensymd 8952	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ (𝐴 ⊔ (har‘𝐴)))
95		entr 8953	. . . 4 ⊢ ((𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴 ∧ 𝒫 𝐴 ≈ (𝐴 ⊔ (har‘𝐴))) → 𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
96	66, 94, 95	syl2anc 585	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
97		endom 8926	. . 3 ⊢ (𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)) → 𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ (har‘𝐴)))
98		pwdjudom 10137	. . 3 ⊢ (𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ (har‘𝐴)) → 𝒫 𝐴 ≼ (har‘𝐴))
99	96, 97, 98	3syl 18	. 2 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≼ (har‘𝐴))
100		sbth 9035	. 2 ⊢ (((har‘𝐴) ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ (har‘𝐴)) → (har‘𝐴) ≈ 𝒫 𝐴)
101	62, 99, 100	syl2anc 585	1 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≈ 𝒫 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ w3a 1087   ∈ wcel 2114  Vcvv 3429  𝒫 cpw 4541   class class class wbr 5085   × cxp 5629  Oncon0 6323  ‘cfv 6498  ωcom 7817   ≈ cen 8890   ≼ cdom 8891   ≺ csdm 8892  Fincfn 8893  harchar 9471   ≼^* cwdom 9479   ⊔ cdju 9822  GCHcgch 10543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-inf2 9562

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-seqom 8387  df-1o 8405  df-2o 8406  df-oadd 8409  df-omul 8410  df-oexp 8411  df-er 8643  df-map 8775  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-oi 9425  df-har 9472  df-wdom 9480  df-cnf 9583  df-dju 9825  df-card 9863  df-fin4 10209  df-gch 10544

This theorem is referenced by:  gchacg  10603