Proof of Theorem pwdjudom
Step | Hyp | Ref
| Expression |
1 | | canthwdom 9119 |
. . . 4
⊢ ¬
𝒫 𝐴
≼* 𝐴 |
2 | | 0ex 5176 |
. . . . . 6
⊢ ∅
∈ V |
3 | | reldom 8564 |
. . . . . . . . 9
⊢ Rel
≼ |
4 | 3 | brrelex2i 5581 |
. . . . . . . 8
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝐴 ⊔ 𝐵) ∈ V) |
5 | | djuexb 9414 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ⊔ 𝐵) ∈ V) |
6 | 4, 5 | sylibr 237 |
. . . . . . 7
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
7 | 6 | simpld 498 |
. . . . . 6
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝐴 ∈ V) |
8 | | xpsnen2g 8662 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝐴 ∈ V)
→ ({∅} × 𝐴) ≈ 𝐴) |
9 | 2, 7, 8 | sylancr 590 |
. . . . 5
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → ({∅} × 𝐴) ≈ 𝐴) |
10 | | endom 8585 |
. . . . 5
⊢
(({∅} × 𝐴) ≈ 𝐴 → ({∅} × 𝐴) ≼ 𝐴) |
11 | | domwdom 9114 |
. . . . 5
⊢
(({∅} × 𝐴) ≼ 𝐴 → ({∅} × 𝐴) ≼* 𝐴) |
12 | | wdomtr 9115 |
. . . . . 6
⊢
((𝒫 𝐴
≼* ({∅} × 𝐴) ∧ ({∅} × 𝐴) ≼* 𝐴) → 𝒫 𝐴 ≼* 𝐴) |
13 | 12 | expcom 417 |
. . . . 5
⊢
(({∅} × 𝐴) ≼* 𝐴 → (𝒫 𝐴 ≼* ({∅} ×
𝐴) → 𝒫 𝐴 ≼* 𝐴)) |
14 | 9, 10, 11, 13 | 4syl 19 |
. . . 4
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝒫 𝐴 ≼* ({∅} ×
𝐴) → 𝒫 𝐴 ≼* 𝐴)) |
15 | 1, 14 | mtoi 202 |
. . 3
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → ¬ 𝒫 𝐴 ≼* ({∅} ×
𝐴)) |
16 | | pwdjuen 9684 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) → 𝒫
(𝐴 ⊔ 𝐴) ≈ (𝒫 𝐴 × 𝒫 𝐴)) |
17 | 7, 7, 16 | syl2anc 587 |
. . . . . . . 8
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 (𝐴 ⊔ 𝐴) ≈ (𝒫 𝐴 × 𝒫 𝐴)) |
18 | | domen1 8712 |
. . . . . . . 8
⊢
(𝒫 (𝐴
⊔ 𝐴) ≈
(𝒫 𝐴 ×
𝒫 𝐴) →
(𝒫 (𝐴 ⊔
𝐴) ≼ (𝐴 ⊔ 𝐵) ↔ (𝒫 𝐴 × 𝒫 𝐴) ≼ (𝐴 ⊔ 𝐵))) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) ↔ (𝒫 𝐴 × 𝒫 𝐴) ≼ (𝐴 ⊔ 𝐵))) |
20 | 19 | ibi 270 |
. . . . . 6
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝒫 𝐴 × 𝒫 𝐴) ≼ (𝐴 ⊔ 𝐵)) |
21 | | df-dju 9406 |
. . . . . 6
⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
22 | 20, 21 | breqtrdi 5072 |
. . . . 5
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝒫 𝐴 × 𝒫 𝐴) ≼ (({∅} × 𝐴) ∪ ({1o} ×
𝐵))) |
23 | | unxpwdom 9129 |
. . . . 5
⊢
((𝒫 𝐴
× 𝒫 𝐴)
≼ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) → (𝒫 𝐴 ≼* ({∅}
× 𝐴) ∨ 𝒫
𝐴 ≼ ({1o}
× 𝐵))) |
24 | 22, 23 | syl 17 |
. . . 4
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝒫 𝐴 ≼* ({∅} ×
𝐴) ∨ 𝒫 𝐴 ≼ ({1o}
× 𝐵))) |
25 | 24 | ord 863 |
. . 3
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (¬ 𝒫 𝐴 ≼* ({∅} ×
𝐴) → 𝒫 𝐴 ≼ ({1o}
× 𝐵))) |
26 | 15, 25 | mpd 15 |
. 2
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 𝐴 ≼ ({1o} × 𝐵)) |
27 | | 1on 8141 |
. . 3
⊢
1o ∈ On |
28 | 6 | simprd 499 |
. . 3
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝐵 ∈ V) |
29 | | xpsnen2g 8662 |
. . 3
⊢
((1o ∈ On ∧ 𝐵 ∈ V) → ({1o} ×
𝐵) ≈ 𝐵) |
30 | 27, 28, 29 | sylancr 590 |
. 2
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → ({1o} × 𝐵) ≈ 𝐵) |
31 | | domentr 8617 |
. 2
⊢
((𝒫 𝐴
≼ ({1o} × 𝐵) ∧ ({1o} × 𝐵) ≈ 𝐵) → 𝒫 𝐴 ≼ 𝐵) |
32 | 26, 30, 31 | syl2anc 587 |
1
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 𝐴 ≼ 𝐵) |