Proof of Theorem pwdjudom
| Step | Hyp | Ref
| Expression |
| 1 | | canthwdom 9619 |
. . . 4
⊢ ¬
𝒫 𝐴
≼* 𝐴 |
| 2 | | 0ex 5307 |
. . . . . 6
⊢ ∅
∈ V |
| 3 | | reldom 8991 |
. . . . . . . . 9
⊢ Rel
≼ |
| 4 | 3 | brrelex2i 5742 |
. . . . . . . 8
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝐴 ⊔ 𝐵) ∈ V) |
| 5 | | djuexb 9949 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ⊔ 𝐵) ∈ V) |
| 6 | 4, 5 | sylibr 234 |
. . . . . . 7
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 7 | 6 | simpld 494 |
. . . . . 6
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝐴 ∈ V) |
| 8 | | xpsnen2g 9105 |
. . . . . 6
⊢ ((∅
∈ V ∧ 𝐴 ∈ V)
→ ({∅} × 𝐴) ≈ 𝐴) |
| 9 | 2, 7, 8 | sylancr 587 |
. . . . 5
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → ({∅} × 𝐴) ≈ 𝐴) |
| 10 | | endom 9019 |
. . . . 5
⊢
(({∅} × 𝐴) ≈ 𝐴 → ({∅} × 𝐴) ≼ 𝐴) |
| 11 | | domwdom 9614 |
. . . . 5
⊢
(({∅} × 𝐴) ≼ 𝐴 → ({∅} × 𝐴) ≼* 𝐴) |
| 12 | | wdomtr 9615 |
. . . . . 6
⊢
((𝒫 𝐴
≼* ({∅} × 𝐴) ∧ ({∅} × 𝐴) ≼* 𝐴) → 𝒫 𝐴 ≼* 𝐴) |
| 13 | 12 | expcom 413 |
. . . . 5
⊢
(({∅} × 𝐴) ≼* 𝐴 → (𝒫 𝐴 ≼* ({∅} ×
𝐴) → 𝒫 𝐴 ≼* 𝐴)) |
| 14 | 9, 10, 11, 13 | 4syl 19 |
. . . 4
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝒫 𝐴 ≼* ({∅} ×
𝐴) → 𝒫 𝐴 ≼* 𝐴)) |
| 15 | 1, 14 | mtoi 199 |
. . 3
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → ¬ 𝒫 𝐴 ≼* ({∅} ×
𝐴)) |
| 16 | | pwdjuen 10222 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) → 𝒫
(𝐴 ⊔ 𝐴) ≈ (𝒫 𝐴 × 𝒫 𝐴)) |
| 17 | 7, 7, 16 | syl2anc 584 |
. . . . . . . 8
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 (𝐴 ⊔ 𝐴) ≈ (𝒫 𝐴 × 𝒫 𝐴)) |
| 18 | | domen1 9159 |
. . . . . . . 8
⊢
(𝒫 (𝐴
⊔ 𝐴) ≈
(𝒫 𝐴 ×
𝒫 𝐴) →
(𝒫 (𝐴 ⊔
𝐴) ≼ (𝐴 ⊔ 𝐵) ↔ (𝒫 𝐴 × 𝒫 𝐴) ≼ (𝐴 ⊔ 𝐵))) |
| 19 | 17, 18 | syl 17 |
. . . . . . 7
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝒫 (𝐴 ⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) ↔ (𝒫 𝐴 × 𝒫 𝐴) ≼ (𝐴 ⊔ 𝐵))) |
| 20 | 19 | ibi 267 |
. . . . . 6
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝒫 𝐴 × 𝒫 𝐴) ≼ (𝐴 ⊔ 𝐵)) |
| 21 | | df-dju 9941 |
. . . . . 6
⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
| 22 | 20, 21 | breqtrdi 5184 |
. . . . 5
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝒫 𝐴 × 𝒫 𝐴) ≼ (({∅} × 𝐴) ∪ ({1o} ×
𝐵))) |
| 23 | | unxpwdom 9629 |
. . . . 5
⊢
((𝒫 𝐴
× 𝒫 𝐴)
≼ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) → (𝒫 𝐴 ≼* ({∅}
× 𝐴) ∨ 𝒫
𝐴 ≼ ({1o}
× 𝐵))) |
| 24 | 22, 23 | syl 17 |
. . . 4
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (𝒫 𝐴 ≼* ({∅} ×
𝐴) ∨ 𝒫 𝐴 ≼ ({1o}
× 𝐵))) |
| 25 | 24 | ord 865 |
. . 3
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → (¬ 𝒫 𝐴 ≼* ({∅} ×
𝐴) → 𝒫 𝐴 ≼ ({1o}
× 𝐵))) |
| 26 | 15, 25 | mpd 15 |
. 2
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 𝐴 ≼ ({1o} × 𝐵)) |
| 27 | | 1on 8518 |
. . 3
⊢
1o ∈ On |
| 28 | 6 | simprd 495 |
. . 3
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝐵 ∈ V) |
| 29 | | xpsnen2g 9105 |
. . 3
⊢
((1o ∈ On ∧ 𝐵 ∈ V) → ({1o} ×
𝐵) ≈ 𝐵) |
| 30 | 27, 28, 29 | sylancr 587 |
. 2
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → ({1o} × 𝐵) ≈ 𝐵) |
| 31 | | domentr 9053 |
. 2
⊢
((𝒫 𝐴
≼ ({1o} × 𝐵) ∧ ({1o} × 𝐵) ≈ 𝐵) → 𝒫 𝐴 ≼ 𝐵) |
| 32 | 26, 30, 31 | syl2anc 584 |
1
⊢
(𝒫 (𝐴
⊔ 𝐴) ≼ (𝐴 ⊔ 𝐵) → 𝒫 𝐴 ≼ 𝐵) |