Proof of Theorem gchpwdom
Step | Hyp | Ref
| Expression |
1 | | simpl2 1058 |
. . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → 𝐴 ∈ GCH) |
2 | | pwexg 4776 |
. . . . . . 7
⊢ (𝐴 ∈ GCH → 𝒫
𝐴 ∈
V) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → 𝒫 𝐴 ∈ V) |
4 | | simpl3 1059 |
. . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → 𝐵 ∈ GCH) |
5 | | cdadom3 8893 |
. . . . . 6
⊢
((𝒫 𝐴 ∈
V ∧ 𝐵 ∈ GCH)
→ 𝒫 𝐴 ≼
(𝒫 𝐴
+𝑐 𝐵)) |
6 | 3, 4, 5 | syl2anc 691 |
. . . . 5
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → 𝒫 𝐴 ≼ (𝒫 𝐴 +𝑐 𝐵)) |
7 | | domen2 7988 |
. . . . 5
⊢ (𝐵 ≈ (𝒫 𝐴 +𝑐 𝐵) → (𝒫 𝐴 ≼ 𝐵 ↔ 𝒫 𝐴 ≼ (𝒫 𝐴 +𝑐 𝐵))) |
8 | 6, 7 | syl5ibrcom 236 |
. . . 4
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝐵 ≈ (𝒫 𝐴 +𝑐 𝐵) → 𝒫 𝐴 ≼ 𝐵)) |
9 | | cdacomen 8886 |
. . . . . . 7
⊢ (𝐵 +𝑐 𝒫
𝐴) ≈ (𝒫 𝐴 +𝑐 𝐵) |
10 | | entr 7894 |
. . . . . . 7
⊢ (((𝐵 +𝑐 𝒫
𝐴) ≈ (𝒫 𝐴 +𝑐 𝐵) ∧ (𝒫 𝐴 +𝑐 𝐵) ≈ 𝒫 𝐵) → (𝐵 +𝑐 𝒫 𝐴) ≈ 𝒫 𝐵) |
11 | 9, 10 | mpan 702 |
. . . . . 6
⊢
((𝒫 𝐴
+𝑐 𝐵)
≈ 𝒫 𝐵 →
(𝐵 +𝑐
𝒫 𝐴) ≈
𝒫 𝐵) |
12 | | ensym 7891 |
. . . . . 6
⊢ ((𝐵 +𝑐 𝒫
𝐴) ≈ 𝒫 𝐵 → 𝒫 𝐵 ≈ (𝐵 +𝑐 𝒫 𝐴)) |
13 | | endom 7868 |
. . . . . 6
⊢
(𝒫 𝐵 ≈
(𝐵 +𝑐
𝒫 𝐴) →
𝒫 𝐵 ≼ (𝐵 +𝑐 𝒫
𝐴)) |
14 | 11, 12, 13 | 3syl 18 |
. . . . 5
⊢
((𝒫 𝐴
+𝑐 𝐵)
≈ 𝒫 𝐵 →
𝒫 𝐵 ≼ (𝐵 +𝑐 𝒫
𝐴)) |
15 | | domsdomtr 7980 |
. . . . . . . . . . 11
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≺ 𝐵) → ω ≺ 𝐵) |
16 | 15 | 3ad2antl1 1216 |
. . . . . . . . . 10
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → ω ≺ 𝐵) |
17 | | sdomnsym 7970 |
. . . . . . . . . 10
⊢ (ω
≺ 𝐵 → ¬
𝐵 ≺
ω) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → ¬ 𝐵 ≺ ω) |
19 | | isfinite 8432 |
. . . . . . . . 9
⊢ (𝐵 ∈ Fin ↔ 𝐵 ≺
ω) |
20 | 18, 19 | sylnibr 318 |
. . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → ¬ 𝐵 ∈ Fin) |
21 | | gchcdaidm 9369 |
. . . . . . . 8
⊢ ((𝐵 ∈ GCH ∧ ¬ 𝐵 ∈ Fin) → (𝐵 +𝑐 𝐵) ≈ 𝐵) |
22 | 4, 20, 21 | syl2anc 691 |
. . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝐵 +𝑐 𝐵) ≈ 𝐵) |
23 | | pwen 8018 |
. . . . . . 7
⊢ ((𝐵 +𝑐 𝐵) ≈ 𝐵 → 𝒫 (𝐵 +𝑐 𝐵) ≈ 𝒫 𝐵) |
24 | | domen1 7987 |
. . . . . . 7
⊢
(𝒫 (𝐵
+𝑐 𝐵)
≈ 𝒫 𝐵 →
(𝒫 (𝐵
+𝑐 𝐵)
≼ (𝐵
+𝑐 𝒫 𝐴) ↔ 𝒫 𝐵 ≼ (𝐵 +𝑐 𝒫 𝐴))) |
25 | 22, 23, 24 | 3syl 18 |
. . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 (𝐵 +𝑐 𝐵) ≼ (𝐵 +𝑐 𝒫 𝐴) ↔ 𝒫 𝐵 ≼ (𝐵 +𝑐 𝒫 𝐴))) |
26 | | pwcdadom 8921 |
. . . . . . 7
⊢
(𝒫 (𝐵
+𝑐 𝐵)
≼ (𝐵
+𝑐 𝒫 𝐴) → 𝒫 𝐵 ≼ 𝒫 𝐴) |
27 | | canth2g 7999 |
. . . . . . . . 9
⊢ (𝐵 ∈ GCH → 𝐵 ≺ 𝒫 𝐵) |
28 | | sdomdomtr 7978 |
. . . . . . . . . 10
⊢ ((𝐵 ≺ 𝒫 𝐵 ∧ 𝒫 𝐵 ≼ 𝒫 𝐴) → 𝐵 ≺ 𝒫 𝐴) |
29 | 28 | ex 449 |
. . . . . . . . 9
⊢ (𝐵 ≺ 𝒫 𝐵 → (𝒫 𝐵 ≼ 𝒫 𝐴 → 𝐵 ≺ 𝒫 𝐴)) |
30 | 4, 27, 29 | 3syl 18 |
. . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 𝐵 ≼ 𝒫 𝐴 → 𝐵 ≺ 𝒫 𝐴)) |
31 | | gchi 9325 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴) → 𝐴 ∈ Fin) |
32 | 31 | 3expia 1259 |
. . . . . . . . 9
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ≺ 𝐵) → (𝐵 ≺ 𝒫 𝐴 → 𝐴 ∈ Fin)) |
33 | 32 | 3ad2antl2 1217 |
. . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝐵 ≺ 𝒫 𝐴 → 𝐴 ∈ Fin)) |
34 | | isfinite 8432 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin ↔ 𝐴 ≺
ω) |
35 | | simpl1 1057 |
. . . . . . . . . . 11
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → ω ≼ 𝐴) |
36 | | domnsym 7971 |
. . . . . . . . . . 11
⊢ (ω
≼ 𝐴 → ¬
𝐴 ≺
ω) |
37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → ¬ 𝐴 ≺ ω) |
38 | 37 | pm2.21d 117 |
. . . . . . . . 9
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝐴 ≺ ω → 𝒫 𝐴 ≼ 𝐵)) |
39 | 34, 38 | syl5bi 231 |
. . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝐴 ∈ Fin → 𝒫 𝐴 ≼ 𝐵)) |
40 | 30, 33, 39 | 3syld 58 |
. . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 𝐵 ≼ 𝒫 𝐴 → 𝒫 𝐴 ≼ 𝐵)) |
41 | 26, 40 | syl5 33 |
. . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 (𝐵 +𝑐 𝐵) ≼ (𝐵 +𝑐 𝒫 𝐴) → 𝒫 𝐴 ≼ 𝐵)) |
42 | 25, 41 | sylbird 249 |
. . . . 5
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 𝐵 ≼ (𝐵 +𝑐 𝒫 𝐴) → 𝒫 𝐴 ≼ 𝐵)) |
43 | 14, 42 | syl5 33 |
. . . 4
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → ((𝒫 𝐴 +𝑐 𝐵) ≈ 𝒫 𝐵 → 𝒫 𝐴 ≼ 𝐵)) |
44 | | cdadom3 8893 |
. . . . . . 7
⊢ ((𝐵 ∈ GCH ∧ 𝒫
𝐴 ∈ V) → 𝐵 ≼ (𝐵 +𝑐 𝒫 𝐴)) |
45 | 4, 3, 44 | syl2anc 691 |
. . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → 𝐵 ≼ (𝐵 +𝑐 𝒫 𝐴)) |
46 | | domentr 7901 |
. . . . . 6
⊢ ((𝐵 ≼ (𝐵 +𝑐 𝒫 𝐴) ∧ (𝐵 +𝑐 𝒫 𝐴) ≈ (𝒫 𝐴 +𝑐 𝐵)) → 𝐵 ≼ (𝒫 𝐴 +𝑐 𝐵)) |
47 | 45, 9, 46 | sylancl 693 |
. . . . 5
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → 𝐵 ≼ (𝒫 𝐴 +𝑐 𝐵)) |
48 | | sdomdom 7869 |
. . . . . . . . 9
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) |
49 | 48 | adantl 481 |
. . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → 𝐴 ≼ 𝐵) |
50 | | pwdom 7997 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝐵 → 𝒫 𝐴 ≼ 𝒫 𝐵) |
51 | | cdadom1 8891 |
. . . . . . . 8
⊢
(𝒫 𝐴 ≼
𝒫 𝐵 →
(𝒫 𝐴
+𝑐 𝐵)
≼ (𝒫 𝐵
+𝑐 𝐵)) |
52 | 49, 50, 51 | 3syl 18 |
. . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 𝐴 +𝑐 𝐵) ≼ (𝒫 𝐵 +𝑐 𝐵)) |
53 | 4, 27 | syl 17 |
. . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → 𝐵 ≺ 𝒫 𝐵) |
54 | | sdomdom 7869 |
. . . . . . . 8
⊢ (𝐵 ≺ 𝒫 𝐵 → 𝐵 ≼ 𝒫 𝐵) |
55 | | cdadom2 8892 |
. . . . . . . 8
⊢ (𝐵 ≼ 𝒫 𝐵 → (𝒫 𝐵 +𝑐 𝐵) ≼ (𝒫 𝐵 +𝑐 𝒫
𝐵)) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 𝐵 +𝑐 𝐵) ≼ (𝒫 𝐵 +𝑐 𝒫 𝐵)) |
57 | | domtr 7895 |
. . . . . . 7
⊢
(((𝒫 𝐴
+𝑐 𝐵)
≼ (𝒫 𝐵
+𝑐 𝐵)
∧ (𝒫 𝐵
+𝑐 𝐵)
≼ (𝒫 𝐵
+𝑐 𝒫 𝐵)) → (𝒫 𝐴 +𝑐 𝐵) ≼ (𝒫 𝐵 +𝑐 𝒫 𝐵)) |
58 | 52, 56, 57 | syl2anc 691 |
. . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 𝐴 +𝑐 𝐵) ≼ (𝒫 𝐵 +𝑐 𝒫 𝐵)) |
59 | | pwcda1 8899 |
. . . . . . . 8
⊢ (𝐵 ∈ GCH → (𝒫
𝐵 +𝑐
𝒫 𝐵) ≈
𝒫 (𝐵
+𝑐 1𝑜)) |
60 | 4, 59 | syl 17 |
. . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 𝐵 +𝑐 𝒫 𝐵) ≈ 𝒫 (𝐵 +𝑐
1𝑜)) |
61 | | gchcda1 9357 |
. . . . . . . . 9
⊢ ((𝐵 ∈ GCH ∧ ¬ 𝐵 ∈ Fin) → (𝐵 +𝑐
1𝑜) ≈ 𝐵) |
62 | 4, 20, 61 | syl2anc 691 |
. . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝐵 +𝑐
1𝑜) ≈ 𝐵) |
63 | | pwen 8018 |
. . . . . . . 8
⊢ ((𝐵 +𝑐
1𝑜) ≈ 𝐵 → 𝒫 (𝐵 +𝑐
1𝑜) ≈ 𝒫 𝐵) |
64 | 62, 63 | syl 17 |
. . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → 𝒫 (𝐵 +𝑐
1𝑜) ≈ 𝒫 𝐵) |
65 | | entr 7894 |
. . . . . . 7
⊢
(((𝒫 𝐵
+𝑐 𝒫 𝐵) ≈ 𝒫 (𝐵 +𝑐
1𝑜) ∧ 𝒫 (𝐵 +𝑐
1𝑜) ≈ 𝒫 𝐵) → (𝒫 𝐵 +𝑐 𝒫 𝐵) ≈ 𝒫 𝐵) |
66 | 60, 64, 65 | syl2anc 691 |
. . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 𝐵 +𝑐 𝒫 𝐵) ≈ 𝒫 𝐵) |
67 | | domentr 7901 |
. . . . . 6
⊢
(((𝒫 𝐴
+𝑐 𝐵)
≼ (𝒫 𝐵
+𝑐 𝒫 𝐵) ∧ (𝒫 𝐵 +𝑐 𝒫 𝐵) ≈ 𝒫 𝐵) → (𝒫 𝐴 +𝑐 𝐵) ≼ 𝒫 𝐵) |
68 | 58, 66, 67 | syl2anc 691 |
. . . . 5
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝒫 𝐴 +𝑐 𝐵) ≼ 𝒫 𝐵) |
69 | | gchor 9328 |
. . . . 5
⊢ (((𝐵 ∈ GCH ∧ ¬ 𝐵 ∈ Fin) ∧ (𝐵 ≼ (𝒫 𝐴 +𝑐 𝐵) ∧ (𝒫 𝐴 +𝑐 𝐵) ≼ 𝒫 𝐵)) → (𝐵 ≈ (𝒫 𝐴 +𝑐 𝐵) ∨ (𝒫 𝐴 +𝑐 𝐵) ≈ 𝒫 𝐵)) |
70 | 4, 20, 47, 68, 69 | syl22anc 1319 |
. . . 4
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → (𝐵 ≈ (𝒫 𝐴 +𝑐 𝐵) ∨ (𝒫 𝐴 +𝑐 𝐵) ≈ 𝒫 𝐵)) |
71 | 8, 43, 70 | mpjaod 395 |
. . 3
⊢
(((ω ≼ 𝐴
∧ 𝐴 ∈ GCH ∧
𝐵 ∈ GCH) ∧ 𝐴 ≺ 𝐵) → 𝒫 𝐴 ≼ 𝐵) |
72 | 71 | ex 449 |
. 2
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) → (𝐴 ≺ 𝐵 → 𝒫 𝐴 ≼ 𝐵)) |
73 | | reldom 7847 |
. . . . 5
⊢ Rel
≼ |
74 | 73 | brrelexi 5082 |
. . . 4
⊢
(𝒫 𝐴 ≼
𝐵 → 𝒫 𝐴 ∈ V) |
75 | | pwexb 6867 |
. . . . 5
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) |
76 | | canth2g 7999 |
. . . . 5
⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴) |
77 | 75, 76 | sylbir 224 |
. . . 4
⊢
(𝒫 𝐴 ∈
V → 𝐴 ≺
𝒫 𝐴) |
78 | 74, 77 | syl 17 |
. . 3
⊢
(𝒫 𝐴 ≼
𝐵 → 𝐴 ≺ 𝒫 𝐴) |
79 | | sdomdomtr 7978 |
. . 3
⊢ ((𝐴 ≺ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ 𝐵) → 𝐴 ≺ 𝐵) |
80 | 78, 79 | mpancom 700 |
. 2
⊢
(𝒫 𝐴 ≼
𝐵 → 𝐴 ≺ 𝐵) |
81 | 72, 80 | impbid1 214 |
1
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) → (𝐴 ≺ 𝐵 ↔ 𝒫 𝐴 ≼ 𝐵)) |