Metamath Proof Explorer

Theorem gchpwdom

Description: A relationship between dominance over the powerset and strict dominance when the sets involved are infinite GCH-sets. Proposition 3.1 of KanamoriPincus p. 421. (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Assertion gchpwdom ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH → A ≺ B ↔ 𝒫 A ≼ B

Proof

Step Hyp Ref Expression
1 simpl2 ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → A ∈ GCH
2 1 pwexd ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 A ∈ V
3 simpl3 ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → B ∈ GCH
4 djudoml ⊢ 𝒫 A ∈ V ∧ B ∈ GCH → 𝒫 A ≼ 𝒫 A ⊔︀ B
5 2 3 4 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 A ≼ 𝒫 A ⊔︀ B
6 domen2 ⊢ B ≈ 𝒫 A ⊔︀ B → 𝒫 A ≼ B ↔ 𝒫 A ≼ 𝒫 A ⊔︀ B
7 5 6 syl5ibrcom ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → B ≈ 𝒫 A ⊔︀ B → 𝒫 A ≼ B
8 djucomen ⊢ B ∈ GCH ∧ 𝒫 A ∈ V → B ⊔︀ 𝒫 A ≈ 𝒫 A ⊔︀ B
9 3 2 8 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → B ⊔︀ 𝒫 A ≈ 𝒫 A ⊔︀ B
10 entr ⊢ B ⊔︀ 𝒫 A ≈ 𝒫 A ⊔︀ B ∧ 𝒫 A ⊔︀ B ≈ 𝒫 B → B ⊔︀ 𝒫 A ≈ 𝒫 B
11 10 ex ⊢ B ⊔︀ 𝒫 A ≈ 𝒫 A ⊔︀ B → 𝒫 A ⊔︀ B ≈ 𝒫 B → B ⊔︀ 𝒫 A ≈ 𝒫 B
12 9 11 syl ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 A ⊔︀ B ≈ 𝒫 B → B ⊔︀ 𝒫 A ≈ 𝒫 B
13 ensym ⊢ B ⊔︀ 𝒫 A ≈ 𝒫 B → 𝒫 B ≈ B ⊔︀ 𝒫 A
14 endom ⊢ 𝒫 B ≈ B ⊔︀ 𝒫 A → 𝒫 B ≼ B ⊔︀ 𝒫 A
15 13 14 syl ⊢ B ⊔︀ 𝒫 A ≈ 𝒫 B → 𝒫 B ≼ B ⊔︀ 𝒫 A
16 12 15 syl6 ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 A ⊔︀ B ≈ 𝒫 B → 𝒫 B ≼ B ⊔︀ 𝒫 A
17 domsdomtr ⊢ ω ≼ A ∧ A ≺ B → ω ≺ B
18 17 3ad2antl1 ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → ω ≺ B
19 sdomnsym ⊢ ω ≺ B → ¬ B ≺ ω
20 18 19 syl ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → ¬ B ≺ ω
21 isfinite ⊢ B ∈ Fin ↔ B ≺ ω
22 20 21 sylnibr ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → ¬ B ∈ Fin
23 gchdjuidm ⊢ B ∈ GCH ∧ ¬ B ∈ Fin → B ⊔︀ B ≈ B
24 3 22 23 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → B ⊔︀ B ≈ B
25 pwen ⊢ B ⊔︀ B ≈ B → 𝒫 B ⊔︀ B ≈ 𝒫 B
26 domen1 ⊢ 𝒫 B ⊔︀ B ≈ 𝒫 B → 𝒫 B ⊔︀ B ≼ B ⊔︀ 𝒫 A ↔ 𝒫 B ≼ B ⊔︀ 𝒫 A
27 24 25 26 3syl ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 B ⊔︀ B ≼ B ⊔︀ 𝒫 A ↔ 𝒫 B ≼ B ⊔︀ 𝒫 A
28 pwdjudom ⊢ 𝒫 B ⊔︀ B ≼ B ⊔︀ 𝒫 A → 𝒫 B ≼ 𝒫 A
29 canth2g ⊢ B ∈ GCH → B ≺ 𝒫 B
30 sdomdomtr ⊢ B ≺ 𝒫 B ∧ 𝒫 B ≼ 𝒫 A → B ≺ 𝒫 A
31 30 ex ⊢ B ≺ 𝒫 B → 𝒫 B ≼ 𝒫 A → B ≺ 𝒫 A
32 3 29 31 3syl ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 B ≼ 𝒫 A → B ≺ 𝒫 A
33 gchi ⊢ A ∈ GCH ∧ A ≺ B ∧ B ≺ 𝒫 A → A ∈ Fin
34 33 3expia ⊢ A ∈ GCH ∧ A ≺ B → B ≺ 𝒫 A → A ∈ Fin
35 34 3ad2antl2 ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → B ≺ 𝒫 A → A ∈ Fin
36 isfinite ⊢ A ∈ Fin ↔ A ≺ ω
37 simpl1 ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → ω ≼ A
38 domnsym ⊢ ω ≼ A → ¬ A ≺ ω
39 37 38 syl ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → ¬ A ≺ ω
40 39 pm2.21d ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → A ≺ ω → 𝒫 A ≼ B
41 36 40 biimtrid ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → A ∈ Fin → 𝒫 A ≼ B
42 32 35 41 3syld ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 B ≼ 𝒫 A → 𝒫 A ≼ B
43 28 42 syl5 ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 B ⊔︀ B ≼ B ⊔︀ 𝒫 A → 𝒫 A ≼ B
44 27 43 sylbird ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 B ≼ B ⊔︀ 𝒫 A → 𝒫 A ≼ B
45 16 44 syld ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 A ⊔︀ B ≈ 𝒫 B → 𝒫 A ≼ B
46 djudoml ⊢ B ∈ GCH ∧ 𝒫 A ∈ V → B ≼ B ⊔︀ 𝒫 A
47 3 2 46 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → B ≼ B ⊔︀ 𝒫 A
48 domentr ⊢ B ≼ B ⊔︀ 𝒫 A ∧ B ⊔︀ 𝒫 A ≈ 𝒫 A ⊔︀ B → B ≼ 𝒫 A ⊔︀ B
49 47 9 48 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → B ≼ 𝒫 A ⊔︀ B
50 sdomdom ⊢ A ≺ B → A ≼ B
51 50 adantl ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → A ≼ B
52 pwdom ⊢ A ≼ B → 𝒫 A ≼ 𝒫 B
53 51 52 syl ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 A ≼ 𝒫 B
54 djudom1 ⊢ 𝒫 A ≼ 𝒫 B ∧ B ∈ GCH → 𝒫 A ⊔︀ B ≼ 𝒫 B ⊔︀ B
55 53 3 54 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 A ⊔︀ B ≼ 𝒫 B ⊔︀ B
56 sdomdom ⊢ B ≺ 𝒫 B → B ≼ 𝒫 B
57 3 29 56 3syl ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → B ≼ 𝒫 B
58 3 pwexd ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 B ∈ V
59 djudom2 ⊢ B ≼ 𝒫 B ∧ 𝒫 B ∈ V → 𝒫 B ⊔︀ B ≼ 𝒫 B ⊔︀ 𝒫 B
60 57 58 59 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 B ⊔︀ B ≼ 𝒫 B ⊔︀ 𝒫 B
61 domtr ⊢ 𝒫 A ⊔︀ B ≼ 𝒫 B ⊔︀ B ∧ 𝒫 B ⊔︀ B ≼ 𝒫 B ⊔︀ 𝒫 B → 𝒫 A ⊔︀ B ≼ 𝒫 B ⊔︀ 𝒫 B
62 55 60 61 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 A ⊔︀ B ≼ 𝒫 B ⊔︀ 𝒫 B
63 pwdju1 ⊢ B ∈ GCH → 𝒫 B ⊔︀ 𝒫 B ≈ 𝒫 B ⊔︀ 1 𝑜
64 3 63 syl ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 B ⊔︀ 𝒫 B ≈ 𝒫 B ⊔︀ 1 𝑜
65 gchdju1 ⊢ B ∈ GCH ∧ ¬ B ∈ Fin → B ⊔︀ 1 𝑜 ≈ B
66 3 22 65 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → B ⊔︀ 1 𝑜 ≈ B
67 pwen ⊢ B ⊔︀ 1 𝑜 ≈ B → 𝒫 B ⊔︀ 1 𝑜 ≈ 𝒫 B
68 66 67 syl ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 B ⊔︀ 1 𝑜 ≈ 𝒫 B
69 entr ⊢ 𝒫 B ⊔︀ 𝒫 B ≈ 𝒫 B ⊔︀ 1 𝑜 ∧ 𝒫 B ⊔︀ 1 𝑜 ≈ 𝒫 B → 𝒫 B ⊔︀ 𝒫 B ≈ 𝒫 B
70 64 68 69 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 B ⊔︀ 𝒫 B ≈ 𝒫 B
71 domentr ⊢ 𝒫 A ⊔︀ B ≼ 𝒫 B ⊔︀ 𝒫 B ∧ 𝒫 B ⊔︀ 𝒫 B ≈ 𝒫 B → 𝒫 A ⊔︀ B ≼ 𝒫 B
72 62 70 71 syl2anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 A ⊔︀ B ≼ 𝒫 B
73 gchor ⊢ B ∈ GCH ∧ ¬ B ∈ Fin ∧ B ≼ 𝒫 A ⊔︀ B ∧ 𝒫 A ⊔︀ B ≼ 𝒫 B → B ≈ 𝒫 A ⊔︀ B ∨ 𝒫 A ⊔︀ B ≈ 𝒫 B
74 3 22 49 72 73 syl22anc ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → B ≈ 𝒫 A ⊔︀ B ∨ 𝒫 A ⊔︀ B ≈ 𝒫 B
75 7 45 74 mpjaod ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH ∧ A ≺ B → 𝒫 A ≼ B
76 75 ex ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH → A ≺ B → 𝒫 A ≼ B
77 reldom ⊢ Rel ⁡ ≼
78 77 brrelex1i ⊢ 𝒫 A ≼ B → 𝒫 A ∈ V
79 pwexb ⊢ A ∈ V ↔ 𝒫 A ∈ V
80 canth2g ⊢ A ∈ V → A ≺ 𝒫 A
81 79 80 sylbir ⊢ 𝒫 A ∈ V → A ≺ 𝒫 A
82 78 81 syl ⊢ 𝒫 A ≼ B → A ≺ 𝒫 A
83 sdomdomtr ⊢ A ≺ 𝒫 A ∧ 𝒫 A ≼ B → A ≺ B
84 82 83 mpancom ⊢ 𝒫 A ≼ B → A ≺ B
85 76 84 impbid1 ⊢ ω ≼ A ∧ A ∈ GCH ∧ B ∈ GCH → A ≺ B ↔ 𝒫 A ≼ B