Theorem gchhar 10682

Description: A "local" form of gchac 10684. 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 9531	. . . 4 ⊢ (har‘𝐴) ∈ On
2		simp3 1156	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ∈ GCH)
3		djudoml 10187	. . . 4 ⊢ (((har‘𝐴) ∈ On ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝒫 𝐴))
4	1, 2, 3	sylancr 599	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝒫 𝐴))
5		domnsym 9101	. . . . . . . . 9 ⊢ (ω ≼ 𝐴 → ¬ 𝐴 ≺ ω)
6	5	3ad2ant1 1151	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ≺ ω)
7		isfinite 9631	. . . . . . . 8 ⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺ ω)
8	6, 7	sylnibr 332	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ∈ Fin)
9		pwfi 9288	. . . . . . 7 ⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
10	8, 9	sylnib 331	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝒫 𝐴 ∈ Fin)
11		djudoml 10187	. . . . . . 7 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
12	2, 1, 11	sylancl 598	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
13		fvexd 6903	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ∈ V)
14		djuex 9913	. . . . . . . . 9 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ V) → (𝒫 𝐴 ⊔ (har‘𝐴)) ∈ V)
15	2, 13, 14	syl2anc 596	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ∈ V)
16		canth2g 9129	. . . . . . . 8 ⊢ ((𝒫 𝐴 ⊔ (har‘𝐴)) ∈ V → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)))
17	15, 16	syl 18	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)))
18		pwdjuen 10184	. . . . . . . . 9 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)))
19	2, 1, 18	sylancl 598	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)))
20	2	pwexd 5355	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝒫 𝐴 ∈ V)
21		simp2 1155	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ∈ GCH)
22		harwdom 9563	. . . . . . . . . . 11 ⊢ (𝐴 ∈ GCH → (har‘𝐴) ≼* 𝒫 (𝐴 × 𝐴))
23		wdompwdom 9550	. . . . . . . . . . 11 ⊢ ((har‘𝐴) ≼* 𝒫 (𝐴 × 𝐴) → 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴))
24	21, 22, 23	3syl 19	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴))
25		xpdom2g 9071	. . . . . . . . . 10 ⊢ ((𝒫 𝒫 𝐴 ∈ V ∧ 𝒫 (har‘𝐴) ≼ 𝒫 𝒫 (𝐴 × 𝐴)) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
26	20, 24, 25	syl2anc 596	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
27	21, 21	xpexd 7759	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 × 𝐴) ∈ V)
28	27	pwexd 5355	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 × 𝐴) ∈ V)
29		pwdjuen 10184	. . . . . . . . . . . 12 ⊢ ((𝒫 𝐴 ∈ GCH ∧ 𝒫 (𝐴 × 𝐴) ∈ V) → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
30	2, 28, 29	syl2anc 596	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)))
31	30	ensymd 9011	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)))
32		enrefg 8990	. . . . . . . . . . . . . 14 ⊢ (𝒫 𝐴 ∈ GCH → 𝒫 𝐴 ≈ 𝒫 𝐴)
33	2, 32	syl 18	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ 𝒫 𝐴)
34		gchxpidm 10672	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴)
35	21, 8, 34	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 × 𝐴) ≈ 𝐴)
36		pwen 9148	. . . . . . . . . . . . . 14 ⊢ ((𝐴 × 𝐴) ≈ 𝐴 → 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴)
37	35, 36	syl 18	. . . . . . . . . . . . 13 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴)
38		djuen 10172	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝐴 ≈ 𝒫 𝐴 ∧ 𝒫 (𝐴 × 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
39	33, 37, 38	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴))
40		gchdjuidm 10671	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝐴 ∈ GCH ∧ ¬ 𝒫 𝐴 ∈ Fin) → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
41	2, 10, 40	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
42		entr 9012	. . . . . . . . . . . 12 ⊢ (((𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ (𝒫 𝐴 ⊔ 𝒫 𝐴) ∧ (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴)
43	39, 41, 42	syl2anc 596	. . . . . . . . . . 11 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴)
44		pwen 9148	. . . . . . . . . . 11 ⊢ ((𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝐴 → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
45	43, 44	syl 18	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
46		entr 9012	. . . . . . . . . 10 ⊢ (((𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ∧ 𝒫 (𝒫 𝐴 ⊔ 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
47	31, 45, 46	syl2anc 596	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴)
48		domentr 9019	. . . . . . . . 9 ⊢ (((𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ∧ (𝒫 𝒫 𝐴 × 𝒫 𝒫 (𝐴 × 𝐴)) ≈ 𝒫 𝒫 𝐴) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
49	26, 47, 48	syl2anc 596	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
50		endomtr 9018	. . . . . . . 8 ⊢ ((𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ∧ (𝒫 𝒫 𝐴 × 𝒫 (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
51	19, 49, 50	syl2anc 596	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫 𝐴)
52		sdomdomtr 9108	. . . . . . 7 ⊢ (((𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ 𝒫 (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝒫 𝐴) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)
53	17, 51, 52	syl2anc 596	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)
54		gchen1 10628	. . . . . 6 ⊢ (((𝒫 𝐴 ∈ GCH ∧ ¬ 𝒫 𝐴 ∈ Fin) ∧ (𝒫 𝐴 ≼ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≺ 𝒫 𝒫 𝐴)) → 𝒫 𝐴 ≈ (𝒫 𝐴 ⊔ (har‘𝐴)))
55	2, 10, 12, 53, 54	syl22anc 852	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ (𝒫 𝐴 ⊔ (har‘𝐴)))
56		djucomen 10180	. . . . . 6 ⊢ ((𝒫 𝐴 ∈ GCH ∧ (har‘𝐴) ∈ V) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
57	2, 13, 56	syl2anc 596	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
58		entr 9012	. . . . 5 ⊢ ((𝒫 𝐴 ≈ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≈ ((har‘𝐴) ⊔ 𝒫 𝐴)) → 𝒫 𝐴 ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
59	55, 57, 58	syl2anc 596	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ ((har‘𝐴) ⊔ 𝒫 𝐴))
60	59	ensymd 9011	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ((har‘𝐴) ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴)
61		domentr 9019	. . 3 ⊢ (((har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝒫 𝐴) ∧ ((har‘𝐴) ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) → (har‘𝐴) ≼ 𝒫 𝐴)
62	4, 60, 61	syl2anc 596	. 2 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ 𝒫 𝐴)
63		gchdjuidm 10671	. . . . . 6 ⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 𝐴) ≈ 𝐴)
64	21, 8, 63	syl2anc 596	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ 𝐴) ≈ 𝐴)
65		pwen 9148	. . . . 5 ⊢ ((𝐴 ⊔ 𝐴) ≈ 𝐴 → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴)
66	64, 65	syl 18	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴)
67		djudoml 10187	. . . . . . . 8 ⊢ ((𝐴 ∈ GCH ∧ (har‘𝐴) ∈ On) → 𝐴 ≼ (𝐴 ⊔ (har‘𝐴)))
68	21, 1, 67	sylancl 598	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≼ (𝐴 ⊔ (har‘𝐴)))
69		harndom 9534	. . . . . . . 8 ⊢ ¬ (har‘𝐴) ≼ 𝐴
70		djudoml 10187	. . . . . . . . . . 11 ⊢ (((har‘𝐴) ∈ On ∧ 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝐴))
71	1, 21, 70	sylancr 599	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝐴))
72		djucomen 10180	. . . . . . . . . . 11 ⊢ (((har‘𝐴) ∈ On ∧ 𝐴 ∈ GCH) → ((har‘𝐴) ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
73	1, 21, 72	sylancr 599	. . . . . . . . . 10 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ((har‘𝐴) ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
74		domentr 9019	. . . . . . . . . 10 ⊢ (((har‘𝐴) ≼ ((har‘𝐴) ⊔ 𝐴) ∧ ((har‘𝐴) ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴))) → (har‘𝐴) ≼ (𝐴 ⊔ (har‘𝐴)))
75	71, 73, 74	syl2anc 596	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≼ (𝐴 ⊔ (har‘𝐴)))
76		domen2 9118	. . . . . . . . 9 ⊢ (𝐴 ≈ (𝐴 ⊔ (har‘𝐴)) → ((har‘𝐴) ≼ 𝐴 ↔ (har‘𝐴) ≼ (𝐴 ⊔ (har‘𝐴))))
77	75, 76	syl5ibrcom 250	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ≈ (𝐴 ⊔ (har‘𝐴)) → (har‘𝐴) ≼ 𝐴))
78	69, 77	mtoi 202	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → ¬ 𝐴 ≈ (𝐴 ⊔ (har‘𝐴)))
79		brsdom 8980	. . . . . . 7 ⊢ (𝐴 ≺ (𝐴 ⊔ (har‘𝐴)) ↔ (𝐴 ≼ (𝐴 ⊔ (har‘𝐴)) ∧ ¬ 𝐴 ≈ (𝐴 ⊔ (har‘𝐴))))
80	68, 78, 79	sylanbrc 595	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≺ (𝐴 ⊔ (har‘𝐴)))
81		canth2g 9129	. . . . . . . . . 10 ⊢ (𝐴 ∈ GCH → 𝐴 ≺ 𝒫 𝐴)
82		sdomdom 8986	. . . . . . . . . 10 ⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴)
83	21, 81, 82	3syl 19	. . . . . . . . 9 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝐴 ≼ 𝒫 𝐴)
84		djudom1 10185	. . . . . . . . 9 ⊢ ((𝐴 ≼ 𝒫 𝐴 ∧ (har‘𝐴) ∈ On) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
85	83, 1, 84	sylancl 598	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴)))
86		djudom2 10186	. . . . . . . . 9 ⊢ (((har‘𝐴) ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
87	62, 2, 86	syl2anc 596	. . . . . . . 8 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
88		domtr 9013	. . . . . . . 8 ⊢ (((𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ (har‘𝐴)) ∧ (𝒫 𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴)) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
89	85, 87, 88	syl2anc 596	. . . . . . 7 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴))
90		domentr 9019	. . . . . . 7 ⊢ (((𝐴 ⊔ (har‘𝐴)) ≼ (𝒫 𝐴 ⊔ 𝒫 𝐴) ∧ (𝒫 𝐴 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐴) → (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴)
91	89, 41, 90	syl2anc 596	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴)
92		gchen2 10629	. . . . . 6 ⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ (𝐴 ⊔ (har‘𝐴)) ∧ (𝐴 ⊔ (har‘𝐴)) ≼ 𝒫 𝐴)) → (𝐴 ⊔ (har‘𝐴)) ≈ 𝒫 𝐴)
93	21, 8, 80, 91, 92	syl22anc 852	. . . . 5 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (𝐴 ⊔ (har‘𝐴)) ≈ 𝒫 𝐴)
94	93	ensymd 9011	. . . 4 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≈ (𝐴 ⊔ (har‘𝐴)))
95		entr 9012	. . . 4 ⊢ ((𝒫 (𝐴 ⊔ 𝐴) ≈ 𝒫 𝐴 ∧ 𝒫 𝐴 ≈ (𝐴 ⊔ (har‘𝐴))) → 𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
96	66, 94, 95	syl2anc 596	. . 3 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)))
97		endom 8985	. . 3 ⊢ (𝒫 (𝐴 ⊔ 𝐴) ≈ (𝐴 ⊔ (har‘𝐴)) → 𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ (har‘𝐴)))
98		pwdjudom 10217	. . 3 ⊢ (𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ (har‘𝐴)) → 𝒫 𝐴 ≼ (har‘𝐴))
99	96, 97, 98	3syl 19	. 2 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ≼ (har‘𝐴))
100		sbth 9095	. 2 ⊢ (((har‘𝐴) ≼ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ (har‘𝐴)) → (har‘𝐴) ≈ 𝒫 𝐴)
101	62, 99, 100	syl2anc 596	1 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≈ 𝒫 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ w3a 1103   ∈ wcel 2146  Vcvv 3458  𝒫 cpw 4567   class class class wbr 5114   × cxp 5664  Oncon0 6367  ‘cfv 6543  ωcom 7871   ≈ cen 8949   ≼ cdom 8950   ≺ csdm 8951  Fincfn 8952  harchar 9528   ≼^* cwdom 9536   ⊔ cdju 9903  GCHcgch 10623

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-inf2 9620

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4878  df-int 4918  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-se 5620  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-seqom 8444  df-1o 8462  df-2o 8463  df-oadd 8466  df-omul 8467  df-oexp 8468  df-er 8703  df-map 8835  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-fsupp 9332  df-oi 9482  df-har 9529  df-wdom 9537  df-cnf 9641  df-dju 9906  df-card 9944  df-fin4 10289  df-gch 10624

This theorem is used by:  gchacg  10683