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	$⊢ (ω ≼ A \land A \in GCH \land 𝒫 A \in GCH) \to har (A) \approx 𝒫 A$

Proof

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

Metamath Proof Explorer

Theorem gchhar

Proof