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