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 ( ( ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝐵 ∈ GCH ) → ( 𝐴 ≺ 𝐵 ↔ 𝒫 𝐴 ≼ 𝐵 ) )

Proof

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