Step |
Hyp |
Ref |
Expression |
1 |
|
relwdom |
⊢ Rel ≼* |
2 |
1
|
brrelex2i |
⊢ ( 𝑋 ≼* 𝑌 → 𝑌 ∈ V ) |
3 |
2
|
pwexd |
⊢ ( 𝑋 ≼* 𝑌 → 𝒫 𝑌 ∈ V ) |
4 |
|
0ss |
⊢ ∅ ⊆ 𝑌 |
5 |
4
|
sspwi |
⊢ 𝒫 ∅ ⊆ 𝒫 𝑌 |
6 |
|
ssdomg |
⊢ ( 𝒫 𝑌 ∈ V → ( 𝒫 ∅ ⊆ 𝒫 𝑌 → 𝒫 ∅ ≼ 𝒫 𝑌 ) ) |
7 |
3 5 6
|
mpisyl |
⊢ ( 𝑋 ≼* 𝑌 → 𝒫 ∅ ≼ 𝒫 𝑌 ) |
8 |
|
pweq |
⊢ ( 𝑋 = ∅ → 𝒫 𝑋 = 𝒫 ∅ ) |
9 |
8
|
breq1d |
⊢ ( 𝑋 = ∅ → ( 𝒫 𝑋 ≼ 𝒫 𝑌 ↔ 𝒫 ∅ ≼ 𝒫 𝑌 ) ) |
10 |
7 9
|
syl5ibr |
⊢ ( 𝑋 = ∅ → ( 𝑋 ≼* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) ) |
11 |
|
brwdomn0 |
⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) |
12 |
|
vex |
⊢ 𝑧 ∈ V |
13 |
|
fopwdom |
⊢ ( ( 𝑧 ∈ V ∧ 𝑧 : 𝑌 –onto→ 𝑋 ) → 𝒫 𝑋 ≼ 𝒫 𝑌 ) |
14 |
12 13
|
mpan |
⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) |
15 |
14
|
exlimiv |
⊢ ( ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) |
16 |
11 15
|
syl6bi |
⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) ) |
17 |
10 16
|
pm2.61ine |
⊢ ( 𝑋 ≼* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌 ) |