Proof of Theorem pwcdadom
Step | Hyp | Ref
| Expression |
1 | | canthwdom 8367 |
. . . 4
⊢ ¬
𝒫 𝐴
≼* 𝐴 |
2 | | 0elpw 4760 |
. . . . . . . . . . 11
⊢ ∅
∈ 𝒫 (𝐴
+𝑐 𝐴) |
3 | 2 | n0ii 3881 |
. . . . . . . . . 10
⊢ ¬
𝒫 (𝐴
+𝑐 𝐴) =
∅ |
4 | | dom0 7973 |
. . . . . . . . . 10
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ ∅ ↔ 𝒫 (𝐴 +𝑐 𝐴) = ∅) |
5 | 3, 4 | mtbir 312 |
. . . . . . . . 9
⊢ ¬
𝒫 (𝐴
+𝑐 𝐴)
≼ ∅ |
6 | | cdafn 8874 |
. . . . . . . . . . . 12
⊢
+𝑐 Fn (V × V) |
7 | | fndm 5904 |
. . . . . . . . . . . 12
⊢ (
+𝑐 Fn (V × V) → dom +𝑐 = (V
× V)) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . 11
⊢ dom
+𝑐 = (V × V) |
9 | 8 | ndmov 6716 |
. . . . . . . . . 10
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 +𝑐 𝐵) = ∅) |
10 | 9 | breq2d 4595 |
. . . . . . . . 9
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝒫
(𝐴 +𝑐
𝐴) ≼ (𝐴 +𝑐 𝐵) ↔ 𝒫 (𝐴 +𝑐 𝐴) ≼
∅)) |
11 | 5, 10 | mtbiri 316 |
. . . . . . . 8
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → ¬
𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)) |
12 | 11 | con4i 112 |
. . . . . . 7
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ (𝐴 ∈ V ∧
𝐵 ∈
V)) |
13 | 12 | simpld 474 |
. . . . . 6
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ 𝐴 ∈
V) |
14 | | 0ex 4718 |
. . . . . 6
⊢ ∅
∈ V |
15 | | xpsneng 7930 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
16 | 13, 14, 15 | sylancl 693 |
. . . . 5
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ (𝐴 ×
{∅}) ≈ 𝐴) |
17 | | endom 7868 |
. . . . 5
⊢ ((𝐴 × {∅}) ≈
𝐴 → (𝐴 × {∅}) ≼ 𝐴) |
18 | | domwdom 8362 |
. . . . 5
⊢ ((𝐴 × {∅}) ≼
𝐴 → (𝐴 × {∅}) ≼*
𝐴) |
19 | | wdomtr 8363 |
. . . . . 6
⊢
((𝒫 𝐴
≼* (𝐴
× {∅}) ∧ (𝐴
× {∅}) ≼* 𝐴) → 𝒫 𝐴 ≼* 𝐴) |
20 | 19 | expcom 450 |
. . . . 5
⊢ ((𝐴 × {∅})
≼* 𝐴
→ (𝒫 𝐴
≼* (𝐴
× {∅}) → 𝒫 𝐴 ≼* 𝐴)) |
21 | 16, 17, 18, 20 | 4syl 19 |
. . . 4
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ (𝒫 𝐴
≼* (𝐴
× {∅}) → 𝒫 𝐴 ≼* 𝐴)) |
22 | 1, 21 | mtoi 189 |
. . 3
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ ¬ 𝒫 𝐴
≼* (𝐴
× {∅})) |
23 | | pwcdaen 8890 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) → 𝒫
(𝐴 +𝑐
𝐴) ≈ (𝒫 𝐴 × 𝒫 𝐴)) |
24 | 13, 13, 23 | syl2anc 691 |
. . . . . . . 8
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ 𝒫 (𝐴
+𝑐 𝐴)
≈ (𝒫 𝐴
× 𝒫 𝐴)) |
25 | | domen1 7987 |
. . . . . . . 8
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≈ (𝒫 𝐴
× 𝒫 𝐴) →
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
↔ (𝒫 𝐴 ×
𝒫 𝐴) ≼ (𝐴 +𝑐 𝐵))) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ (𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
↔ (𝒫 𝐴 ×
𝒫 𝐴) ≼ (𝐴 +𝑐 𝐵))) |
27 | 26 | ibi 255 |
. . . . . 6
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ (𝒫 𝐴 ×
𝒫 𝐴) ≼ (𝐴 +𝑐 𝐵)) |
28 | | cdaval 8875 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 +𝑐 𝐵) = ((𝐴 × {∅}) ∪ (𝐵 ×
{1𝑜}))) |
29 | 12, 28 | syl 17 |
. . . . . 6
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ (𝐴
+𝑐 𝐵) =
((𝐴 × {∅})
∪ (𝐵 ×
{1𝑜}))) |
30 | 27, 29 | breqtrd 4609 |
. . . . 5
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ (𝒫 𝐴 ×
𝒫 𝐴) ≼
((𝐴 × {∅})
∪ (𝐵 ×
{1𝑜}))) |
31 | | unxpwdom 8377 |
. . . . 5
⊢
((𝒫 𝐴
× 𝒫 𝐴)
≼ ((𝐴 ×
{∅}) ∪ (𝐵 ×
{1𝑜})) → (𝒫 𝐴 ≼* (𝐴 × {∅}) ∨ 𝒫 𝐴 ≼ (𝐵 ×
{1𝑜}))) |
32 | 30, 31 | syl 17 |
. . . 4
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ (𝒫 𝐴
≼* (𝐴
× {∅}) ∨ 𝒫 𝐴 ≼ (𝐵 ×
{1𝑜}))) |
33 | 32 | ord 391 |
. . 3
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ (¬ 𝒫 𝐴
≼* (𝐴
× {∅}) → 𝒫 𝐴 ≼ (𝐵 ×
{1𝑜}))) |
34 | 22, 33 | mpd 15 |
. 2
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ 𝒫 𝐴 ≼
(𝐵 ×
{1𝑜})) |
35 | 12 | simprd 478 |
. . 3
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ 𝐵 ∈
V) |
36 | | 1on 7454 |
. . 3
⊢
1𝑜 ∈ On |
37 | | xpsneng 7930 |
. . 3
⊢ ((𝐵 ∈ V ∧
1𝑜 ∈ On) → (𝐵 × {1𝑜}) ≈
𝐵) |
38 | 35, 36, 37 | sylancl 693 |
. 2
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ (𝐵 ×
{1𝑜}) ≈ 𝐵) |
39 | | domentr 7901 |
. 2
⊢
((𝒫 𝐴
≼ (𝐵 ×
{1𝑜}) ∧ (𝐵 × {1𝑜}) ≈
𝐵) → 𝒫 𝐴 ≼ 𝐵) |
40 | 34, 38, 39 | syl2anc 691 |
1
⊢
(𝒫 (𝐴
+𝑐 𝐴)
≼ (𝐴
+𝑐 𝐵)
→ 𝒫 𝐴 ≼
𝐵) |