MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gchpwdom Structured version   Visualization version   GIF version

Theorem gchpwdom 10662
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.)
Assertion
Ref Expression
gchpwdom ((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) → (𝐴𝐵 ↔ 𝒫 𝐴𝐵))

Proof of Theorem gchpwdom
StepHypRef Expression
1 simpl2 1189 . . . . . . 7 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝐴 ∈ GCH)
21pwexd 5368 . . . . . 6 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝒫 𝐴 ∈ V)
3 simpl3 1190 . . . . . 6 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝐵 ∈ GCH)
4 djudoml 10176 . . . . . 6 ((𝒫 𝐴 ∈ V ∧ 𝐵 ∈ GCH) → 𝒫 𝐴 ≼ (𝒫 𝐴𝐵))
52, 3, 4syl2anc 583 . . . . 5 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝒫 𝐴 ≼ (𝒫 𝐴𝐵))
6 domen2 9117 . . . . 5 (𝐵 ≈ (𝒫 𝐴𝐵) → (𝒫 𝐴𝐵 ↔ 𝒫 𝐴 ≼ (𝒫 𝐴𝐵)))
75, 6syl5ibrcom 246 . . . 4 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝐵 ≈ (𝒫 𝐴𝐵) → 𝒫 𝐴𝐵))
8 djucomen 10169 . . . . . . . 8 ((𝐵 ∈ GCH ∧ 𝒫 𝐴 ∈ V) → (𝐵 ⊔ 𝒫 𝐴) ≈ (𝒫 𝐴𝐵))
93, 2, 8syl2anc 583 . . . . . . 7 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝐵 ⊔ 𝒫 𝐴) ≈ (𝒫 𝐴𝐵))
10 entr 8999 . . . . . . . 8 (((𝐵 ⊔ 𝒫 𝐴) ≈ (𝒫 𝐴𝐵) ∧ (𝒫 𝐴𝐵) ≈ 𝒫 𝐵) → (𝐵 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐵)
1110ex 412 . . . . . . 7 ((𝐵 ⊔ 𝒫 𝐴) ≈ (𝒫 𝐴𝐵) → ((𝒫 𝐴𝐵) ≈ 𝒫 𝐵 → (𝐵 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐵))
129, 11syl 17 . . . . . 6 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → ((𝒫 𝐴𝐵) ≈ 𝒫 𝐵 → (𝐵 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐵))
13 ensym 8996 . . . . . . 7 ((𝐵 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐵 → 𝒫 𝐵 ≈ (𝐵 ⊔ 𝒫 𝐴))
14 endom 8972 . . . . . . 7 (𝒫 𝐵 ≈ (𝐵 ⊔ 𝒫 𝐴) → 𝒫 𝐵 ≼ (𝐵 ⊔ 𝒫 𝐴))
1513, 14syl 17 . . . . . 6 ((𝐵 ⊔ 𝒫 𝐴) ≈ 𝒫 𝐵 → 𝒫 𝐵 ≼ (𝐵 ⊔ 𝒫 𝐴))
1612, 15syl6 35 . . . . 5 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → ((𝒫 𝐴𝐵) ≈ 𝒫 𝐵 → 𝒫 𝐵 ≼ (𝐵 ⊔ 𝒫 𝐴)))
17 domsdomtr 9109 . . . . . . . . . . 11 ((ω ≼ 𝐴𝐴𝐵) → ω ≺ 𝐵)
18173ad2antl1 1182 . . . . . . . . . 10 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → ω ≺ 𝐵)
19 sdomnsym 9095 . . . . . . . . . 10 (ω ≺ 𝐵 → ¬ 𝐵 ≺ ω)
2018, 19syl 17 . . . . . . . . 9 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → ¬ 𝐵 ≺ ω)
21 isfinite 9644 . . . . . . . . 9 (𝐵 ∈ Fin ↔ 𝐵 ≺ ω)
2220, 21sylnibr 329 . . . . . . . 8 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → ¬ 𝐵 ∈ Fin)
23 gchdjuidm 10660 . . . . . . . 8 ((𝐵 ∈ GCH ∧ ¬ 𝐵 ∈ Fin) → (𝐵𝐵) ≈ 𝐵)
243, 22, 23syl2anc 583 . . . . . . 7 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝐵𝐵) ≈ 𝐵)
25 pwen 9147 . . . . . . 7 ((𝐵𝐵) ≈ 𝐵 → 𝒫 (𝐵𝐵) ≈ 𝒫 𝐵)
26 domen1 9116 . . . . . . 7 (𝒫 (𝐵𝐵) ≈ 𝒫 𝐵 → (𝒫 (𝐵𝐵) ≼ (𝐵 ⊔ 𝒫 𝐴) ↔ 𝒫 𝐵 ≼ (𝐵 ⊔ 𝒫 𝐴)))
2724, 25, 263syl 18 . . . . . 6 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 (𝐵𝐵) ≼ (𝐵 ⊔ 𝒫 𝐴) ↔ 𝒫 𝐵 ≼ (𝐵 ⊔ 𝒫 𝐴)))
28 pwdjudom 10208 . . . . . . 7 (𝒫 (𝐵𝐵) ≼ (𝐵 ⊔ 𝒫 𝐴) → 𝒫 𝐵 ≼ 𝒫 𝐴)
29 canth2g 9128 . . . . . . . . 9 (𝐵 ∈ GCH → 𝐵 ≺ 𝒫 𝐵)
30 sdomdomtr 9107 . . . . . . . . . 10 ((𝐵 ≺ 𝒫 𝐵 ∧ 𝒫 𝐵 ≼ 𝒫 𝐴) → 𝐵 ≺ 𝒫 𝐴)
3130ex 412 . . . . . . . . 9 (𝐵 ≺ 𝒫 𝐵 → (𝒫 𝐵 ≼ 𝒫 𝐴𝐵 ≺ 𝒫 𝐴))
323, 29, 313syl 18 . . . . . . . 8 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 𝐵 ≼ 𝒫 𝐴𝐵 ≺ 𝒫 𝐴))
33 gchi 10616 . . . . . . . . . 10 ((𝐴 ∈ GCH ∧ 𝐴𝐵𝐵 ≺ 𝒫 𝐴) → 𝐴 ∈ Fin)
34333expia 1118 . . . . . . . . 9 ((𝐴 ∈ GCH ∧ 𝐴𝐵) → (𝐵 ≺ 𝒫 𝐴𝐴 ∈ Fin))
35343ad2antl2 1183 . . . . . . . 8 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝐵 ≺ 𝒫 𝐴𝐴 ∈ Fin))
36 isfinite 9644 . . . . . . . . 9 (𝐴 ∈ Fin ↔ 𝐴 ≺ ω)
37 simpl1 1188 . . . . . . . . . . 11 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → ω ≼ 𝐴)
38 domnsym 9096 . . . . . . . . . . 11 (ω ≼ 𝐴 → ¬ 𝐴 ≺ ω)
3937, 38syl 17 . . . . . . . . . 10 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → ¬ 𝐴 ≺ ω)
4039pm2.21d 121 . . . . . . . . 9 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝐴 ≺ ω → 𝒫 𝐴𝐵))
4136, 40biimtrid 241 . . . . . . . 8 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝐴 ∈ Fin → 𝒫 𝐴𝐵))
4232, 35, 413syld 60 . . . . . . 7 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 𝐵 ≼ 𝒫 𝐴 → 𝒫 𝐴𝐵))
4328, 42syl5 34 . . . . . 6 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 (𝐵𝐵) ≼ (𝐵 ⊔ 𝒫 𝐴) → 𝒫 𝐴𝐵))
4427, 43sylbird 260 . . . . 5 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 𝐵 ≼ (𝐵 ⊔ 𝒫 𝐴) → 𝒫 𝐴𝐵))
4516, 44syld 47 . . . 4 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → ((𝒫 𝐴𝐵) ≈ 𝒫 𝐵 → 𝒫 𝐴𝐵))
46 djudoml 10176 . . . . . . 7 ((𝐵 ∈ GCH ∧ 𝒫 𝐴 ∈ V) → 𝐵 ≼ (𝐵 ⊔ 𝒫 𝐴))
473, 2, 46syl2anc 583 . . . . . 6 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝐵 ≼ (𝐵 ⊔ 𝒫 𝐴))
48 domentr 9006 . . . . . 6 ((𝐵 ≼ (𝐵 ⊔ 𝒫 𝐴) ∧ (𝐵 ⊔ 𝒫 𝐴) ≈ (𝒫 𝐴𝐵)) → 𝐵 ≼ (𝒫 𝐴𝐵))
4947, 9, 48syl2anc 583 . . . . 5 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝐵 ≼ (𝒫 𝐴𝐵))
50 sdomdom 8973 . . . . . . . . . 10 (𝐴𝐵𝐴𝐵)
5150adantl 481 . . . . . . . . 9 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝐴𝐵)
52 pwdom 9126 . . . . . . . . 9 (𝐴𝐵 → 𝒫 𝐴 ≼ 𝒫 𝐵)
5351, 52syl 17 . . . . . . . 8 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝒫 𝐴 ≼ 𝒫 𝐵)
54 djudom1 10174 . . . . . . . 8 ((𝒫 𝐴 ≼ 𝒫 𝐵𝐵 ∈ GCH) → (𝒫 𝐴𝐵) ≼ (𝒫 𝐵𝐵))
5553, 3, 54syl2anc 583 . . . . . . 7 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 𝐴𝐵) ≼ (𝒫 𝐵𝐵))
56 sdomdom 8973 . . . . . . . . 9 (𝐵 ≺ 𝒫 𝐵𝐵 ≼ 𝒫 𝐵)
573, 29, 563syl 18 . . . . . . . 8 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝐵 ≼ 𝒫 𝐵)
583pwexd 5368 . . . . . . . 8 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝒫 𝐵 ∈ V)
59 djudom2 10175 . . . . . . . 8 ((𝐵 ≼ 𝒫 𝐵 ∧ 𝒫 𝐵 ∈ V) → (𝒫 𝐵𝐵) ≼ (𝒫 𝐵 ⊔ 𝒫 𝐵))
6057, 58, 59syl2anc 583 . . . . . . 7 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 𝐵𝐵) ≼ (𝒫 𝐵 ⊔ 𝒫 𝐵))
61 domtr 9000 . . . . . . 7 (((𝒫 𝐴𝐵) ≼ (𝒫 𝐵𝐵) ∧ (𝒫 𝐵𝐵) ≼ (𝒫 𝐵 ⊔ 𝒫 𝐵)) → (𝒫 𝐴𝐵) ≼ (𝒫 𝐵 ⊔ 𝒫 𝐵))
6255, 60, 61syl2anc 583 . . . . . 6 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 𝐴𝐵) ≼ (𝒫 𝐵 ⊔ 𝒫 𝐵))
63 pwdju1 10182 . . . . . . . 8 (𝐵 ∈ GCH → (𝒫 𝐵 ⊔ 𝒫 𝐵) ≈ 𝒫 (𝐵 ⊔ 1o))
643, 63syl 17 . . . . . . 7 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 𝐵 ⊔ 𝒫 𝐵) ≈ 𝒫 (𝐵 ⊔ 1o))
65 gchdju1 10648 . . . . . . . . 9 ((𝐵 ∈ GCH ∧ ¬ 𝐵 ∈ Fin) → (𝐵 ⊔ 1o) ≈ 𝐵)
663, 22, 65syl2anc 583 . . . . . . . 8 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝐵 ⊔ 1o) ≈ 𝐵)
67 pwen 9147 . . . . . . . 8 ((𝐵 ⊔ 1o) ≈ 𝐵 → 𝒫 (𝐵 ⊔ 1o) ≈ 𝒫 𝐵)
6866, 67syl 17 . . . . . . 7 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝒫 (𝐵 ⊔ 1o) ≈ 𝒫 𝐵)
69 entr 8999 . . . . . . 7 (((𝒫 𝐵 ⊔ 𝒫 𝐵) ≈ 𝒫 (𝐵 ⊔ 1o) ∧ 𝒫 (𝐵 ⊔ 1o) ≈ 𝒫 𝐵) → (𝒫 𝐵 ⊔ 𝒫 𝐵) ≈ 𝒫 𝐵)
7064, 68, 69syl2anc 583 . . . . . 6 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 𝐵 ⊔ 𝒫 𝐵) ≈ 𝒫 𝐵)
71 domentr 9006 . . . . . 6 (((𝒫 𝐴𝐵) ≼ (𝒫 𝐵 ⊔ 𝒫 𝐵) ∧ (𝒫 𝐵 ⊔ 𝒫 𝐵) ≈ 𝒫 𝐵) → (𝒫 𝐴𝐵) ≼ 𝒫 𝐵)
7262, 70, 71syl2anc 583 . . . . 5 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝒫 𝐴𝐵) ≼ 𝒫 𝐵)
73 gchor 10619 . . . . 5 (((𝐵 ∈ GCH ∧ ¬ 𝐵 ∈ Fin) ∧ (𝐵 ≼ (𝒫 𝐴𝐵) ∧ (𝒫 𝐴𝐵) ≼ 𝒫 𝐵)) → (𝐵 ≈ (𝒫 𝐴𝐵) ∨ (𝒫 𝐴𝐵) ≈ 𝒫 𝐵))
743, 22, 49, 72, 73syl22anc 836 . . . 4 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → (𝐵 ≈ (𝒫 𝐴𝐵) ∨ (𝒫 𝐴𝐵) ≈ 𝒫 𝐵))
757, 45, 74mpjaod 857 . . 3 (((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) ∧ 𝐴𝐵) → 𝒫 𝐴𝐵)
7675ex 412 . 2 ((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) → (𝐴𝐵 → 𝒫 𝐴𝐵))
77 reldom 8942 . . . . 5 Rel ≼
7877brrelex1i 5723 . . . 4 (𝒫 𝐴𝐵 → 𝒫 𝐴 ∈ V)
79 pwexb 7747 . . . . 5 (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
80 canth2g 9128 . . . . 5 (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
8179, 80sylbir 234 . . . 4 (𝒫 𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
8278, 81syl 17 . . 3 (𝒫 𝐴𝐵𝐴 ≺ 𝒫 𝐴)
83 sdomdomtr 9107 . . 3 ((𝐴 ≺ 𝒫 𝐴 ∧ 𝒫 𝐴𝐵) → 𝐴𝐵)
8482, 83mpancom 685 . 2 (𝒫 𝐴𝐵𝐴𝐵)
8576, 84impbid1 224 1 ((ω ≼ 𝐴𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) → (𝐴𝐵 ↔ 𝒫 𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844  w3a 1084  wcel 2098  Vcvv 3466  𝒫 cpw 4595   class class class wbr 5139  ωcom 7849  1oc1o 8455  cen 8933  cdom 8934  csdm 8935  Fincfn 8936  cdju 9890  GCHcgch 10612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-inf2 9633
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-tp 4626  df-op 4628  df-uni 4901  df-int 4942  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-se 5623  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-isom 6543  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-1st 7969  df-2nd 7970  df-supp 8142  df-frecs 8262  df-wrecs 8293  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 8700  df-map 8819  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-oi 9502  df-har 9549  df-wdom 9557  df-cnf 9654  df-dju 9893  df-card 9931  df-fin4 10279  df-gch 10613
This theorem is referenced by:  gchaleph2  10664  gchina  10691
  Copyright terms: Public domain W3C validator