Step |
Hyp |
Ref |
Expression |
1 |
|
0elpw |
⊢ ∅ ∈ 𝒫 𝐴 |
2 |
|
ne0i |
⊢ ( ∅ ∈ 𝒫 𝐴 → 𝒫 𝐴 ≠ ∅ ) |
3 |
1 2
|
mp1i |
⊢ ( 𝒫 𝐴 ≼* 𝐴 → 𝒫 𝐴 ≠ ∅ ) |
4 |
|
brwdomn0 |
⊢ ( 𝒫 𝐴 ≠ ∅ → ( 𝒫 𝐴 ≼* 𝐴 ↔ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝒫 𝐴 ) ) |
5 |
3 4
|
syl |
⊢ ( 𝒫 𝐴 ≼* 𝐴 → ( 𝒫 𝐴 ≼* 𝐴 ↔ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝒫 𝐴 ) ) |
6 |
5
|
ibi |
⊢ ( 𝒫 𝐴 ≼* 𝐴 → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝒫 𝐴 ) |
7 |
|
relwdom |
⊢ Rel ≼* |
8 |
7
|
brrelex2i |
⊢ ( 𝒫 𝐴 ≼* 𝐴 → 𝐴 ∈ V ) |
9 |
|
foeq2 |
⊢ ( 𝑥 = 𝐴 → ( 𝑓 : 𝑥 –onto→ 𝒫 𝑥 ↔ 𝑓 : 𝐴 –onto→ 𝒫 𝑥 ) ) |
10 |
|
pweq |
⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 ) |
11 |
|
foeq3 |
⊢ ( 𝒫 𝑥 = 𝒫 𝐴 → ( 𝑓 : 𝐴 –onto→ 𝒫 𝑥 ↔ 𝑓 : 𝐴 –onto→ 𝒫 𝐴 ) ) |
12 |
10 11
|
syl |
⊢ ( 𝑥 = 𝐴 → ( 𝑓 : 𝐴 –onto→ 𝒫 𝑥 ↔ 𝑓 : 𝐴 –onto→ 𝒫 𝐴 ) ) |
13 |
9 12
|
bitrd |
⊢ ( 𝑥 = 𝐴 → ( 𝑓 : 𝑥 –onto→ 𝒫 𝑥 ↔ 𝑓 : 𝐴 –onto→ 𝒫 𝐴 ) ) |
14 |
13
|
notbid |
⊢ ( 𝑥 = 𝐴 → ( ¬ 𝑓 : 𝑥 –onto→ 𝒫 𝑥 ↔ ¬ 𝑓 : 𝐴 –onto→ 𝒫 𝐴 ) ) |
15 |
|
vex |
⊢ 𝑥 ∈ V |
16 |
15
|
canth |
⊢ ¬ 𝑓 : 𝑥 –onto→ 𝒫 𝑥 |
17 |
14 16
|
vtoclg |
⊢ ( 𝐴 ∈ V → ¬ 𝑓 : 𝐴 –onto→ 𝒫 𝐴 ) |
18 |
8 17
|
syl |
⊢ ( 𝒫 𝐴 ≼* 𝐴 → ¬ 𝑓 : 𝐴 –onto→ 𝒫 𝐴 ) |
19 |
18
|
nexdv |
⊢ ( 𝒫 𝐴 ≼* 𝐴 → ¬ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝒫 𝐴 ) |
20 |
6 19
|
pm2.65i |
⊢ ¬ 𝒫 𝐴 ≼* 𝐴 |