Proof of Theorem cdalepw
Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . 3
⊢ (𝐴 = ∅ → (𝐴 +𝑐 𝐵) = (∅
+𝑐 𝐵)) |
2 | 1 | breq1d 4663 |
. 2
⊢ (𝐴 = ∅ → ((𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴 ↔ (∅
+𝑐 𝐵)
≼ 𝒫 𝐴)) |
3 | | relen 7960 |
. . . . . . . . 9
⊢ Rel
≈ |
4 | 3 | brrelex2i 5159 |
. . . . . . . 8
⊢ ((𝐴 +𝑐 𝐴) ≈ 𝐴 → 𝐴 ∈ V) |
5 | 4 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐴 ∈ V) |
6 | | canth2g 8114 |
. . . . . . 7
⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴) |
7 | | sdomdom 7983 |
. . . . . . 7
⊢ (𝐴 ≺ 𝒫 𝐴 → 𝐴 ≼ 𝒫 𝐴) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . 6
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐴 ≼ 𝒫 𝐴) |
9 | | simpr 477 |
. . . . . 6
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ≼ 𝒫 𝐴) |
10 | | cdadom1 9008 |
. . . . . . 7
⊢ (𝐴 ≼ 𝒫 𝐴 → (𝐴 +𝑐 𝐵) ≼ (𝒫 𝐴 +𝑐 𝐵)) |
11 | | cdadom2 9009 |
. . . . . . 7
⊢ (𝐵 ≼ 𝒫 𝐴 → (𝒫 𝐴 +𝑐 𝐵) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) |
12 | | domtr 8009 |
. . . . . . 7
⊢ (((𝐴 +𝑐 𝐵) ≼ (𝒫 𝐴 +𝑐 𝐵) ∧ (𝒫 𝐴 +𝑐 𝐵) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) → (𝐴 +𝑐 𝐵) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴)) |
13 | 10, 11, 12 | syl2an 494 |
. . . . . 6
⊢ ((𝐴 ≼ 𝒫 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 +𝑐 𝐵) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴)) |
14 | 8, 9, 13 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 +𝑐 𝐵) ≼ (𝒫 𝐴 +𝑐 𝒫 𝐴)) |
15 | | pwcda1 9016 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝒫
𝐴 +𝑐
𝒫 𝐴) ≈
𝒫 (𝐴
+𝑐 1𝑜)) |
16 | 5, 15 | syl 17 |
. . . . 5
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝒫 𝐴 +𝑐 𝒫 𝐴) ≈ 𝒫 (𝐴 +𝑐
1𝑜)) |
17 | | domentr 8015 |
. . . . 5
⊢ (((𝐴 +𝑐 𝐵) ≼ (𝒫 𝐴 +𝑐 𝒫
𝐴) ∧ (𝒫 𝐴 +𝑐 𝒫
𝐴) ≈ 𝒫 (𝐴 +𝑐
1𝑜)) → (𝐴 +𝑐 𝐵) ≼ 𝒫 (𝐴 +𝑐
1𝑜)) |
18 | 14, 16, 17 | syl2anc 693 |
. . . 4
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 +𝑐 𝐵) ≼ 𝒫 (𝐴 +𝑐
1𝑜)) |
19 | 18 | adantr 481 |
. . 3
⊢ ((((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≠ ∅) → (𝐴 +𝑐 𝐵) ≼ 𝒫 (𝐴 +𝑐
1𝑜)) |
20 | | 0sdomg 8089 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
21 | 5, 20 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
22 | 21 | biimpar 502 |
. . . . . . 7
⊢ ((((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≠ ∅) → ∅ ≺ 𝐴) |
23 | | 0sdom1dom 8158 |
. . . . . . 7
⊢ (∅
≺ 𝐴 ↔
1𝑜 ≼ 𝐴) |
24 | 22, 23 | sylib 208 |
. . . . . 6
⊢ ((((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≠ ∅) → 1𝑜
≼ 𝐴) |
25 | | cdadom2 9009 |
. . . . . 6
⊢
(1𝑜 ≼ 𝐴 → (𝐴 +𝑐
1𝑜) ≼ (𝐴 +𝑐 𝐴)) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ ((((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≠ ∅) → (𝐴 +𝑐
1𝑜) ≼ (𝐴 +𝑐 𝐴)) |
27 | | simpll 790 |
. . . . 5
⊢ ((((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≠ ∅) → (𝐴 +𝑐 𝐴) ≈ 𝐴) |
28 | | domentr 8015 |
. . . . 5
⊢ (((𝐴 +𝑐
1𝑜) ≼ (𝐴 +𝑐 𝐴) ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴) → (𝐴 +𝑐
1𝑜) ≼ 𝐴) |
29 | 26, 27, 28 | syl2anc 693 |
. . . 4
⊢ ((((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≠ ∅) → (𝐴 +𝑐
1𝑜) ≼ 𝐴) |
30 | | pwdom 8112 |
. . . 4
⊢ ((𝐴 +𝑐
1𝑜) ≼ 𝐴 → 𝒫 (𝐴 +𝑐
1𝑜) ≼ 𝒫 𝐴) |
31 | 29, 30 | syl 17 |
. . 3
⊢ ((((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≠ ∅) → 𝒫 (𝐴 +𝑐
1𝑜) ≼ 𝒫 𝐴) |
32 | | domtr 8009 |
. . 3
⊢ (((𝐴 +𝑐 𝐵) ≼ 𝒫 (𝐴 +𝑐
1𝑜) ∧ 𝒫 (𝐴 +𝑐
1𝑜) ≼ 𝒫 𝐴) → (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴) |
33 | 19, 31, 32 | syl2anc 693 |
. 2
⊢ ((((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) ∧ 𝐴 ≠ ∅) → (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴) |
34 | | cdacomen 9003 |
. . 3
⊢ (∅
+𝑐 𝐵)
≈ (𝐵
+𝑐 ∅) |
35 | | reldom 7961 |
. . . . . . 7
⊢ Rel
≼ |
36 | 35 | brrelexi 5158 |
. . . . . 6
⊢ (𝐵 ≼ 𝒫 𝐴 → 𝐵 ∈ V) |
37 | 36 | adantl 482 |
. . . . 5
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → 𝐵 ∈ V) |
38 | | cda0en 9001 |
. . . . 5
⊢ (𝐵 ∈ V → (𝐵 +𝑐 ∅)
≈ 𝐵) |
39 | | domen1 8102 |
. . . . 5
⊢ ((𝐵 +𝑐 ∅)
≈ 𝐵 → ((𝐵 +𝑐 ∅)
≼ 𝒫 𝐴 ↔
𝐵 ≼ 𝒫 𝐴)) |
40 | 37, 38, 39 | 3syl 18 |
. . . 4
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → ((𝐵 +𝑐 ∅) ≼
𝒫 𝐴 ↔ 𝐵 ≼ 𝒫 𝐴)) |
41 | 9, 40 | mpbird 247 |
. . 3
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐵 +𝑐 ∅) ≼
𝒫 𝐴) |
42 | | endomtr 8014 |
. . 3
⊢
(((∅ +𝑐 𝐵) ≈ (𝐵 +𝑐 ∅) ∧ (𝐵 +𝑐 ∅)
≼ 𝒫 𝐴) →
(∅ +𝑐 𝐵) ≼ 𝒫 𝐴) |
43 | 34, 41, 42 | sylancr 695 |
. 2
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (∅ +𝑐
𝐵) ≼ 𝒫 𝐴) |
44 | 2, 33, 43 | pm2.61ne 2879 |
1
⊢ (((𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 +𝑐 𝐵) ≼ 𝒫 𝐴) |