| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pweq |
|- ( A = (/) -> ~P A = ~P (/) ) |
| 2 |
1
|
breq1d |
|- ( A = (/) -> ( ~P A ~<_ ~P B <-> ~P (/) ~<_ ~P B ) ) |
| 3 |
|
reldom |
|- Rel ~<_ |
| 4 |
3
|
brrelex1i |
|- ( A ~<_ B -> A e. _V ) |
| 5 |
|
0sdomg |
|- ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) ) |
| 6 |
4 5
|
syl |
|- ( A ~<_ B -> ( (/) ~< A <-> A =/= (/) ) ) |
| 7 |
6
|
biimpar |
|- ( ( A ~<_ B /\ A =/= (/) ) -> (/) ~< A ) |
| 8 |
|
simpl |
|- ( ( A ~<_ B /\ A =/= (/) ) -> A ~<_ B ) |
| 9 |
|
fodomr |
|- ( ( (/) ~< A /\ A ~<_ B ) -> E. f f : B -onto-> A ) |
| 10 |
7 8 9
|
syl2anc |
|- ( ( A ~<_ B /\ A =/= (/) ) -> E. f f : B -onto-> A ) |
| 11 |
|
vex |
|- f e. _V |
| 12 |
|
fopwdom |
|- ( ( f e. _V /\ f : B -onto-> A ) -> ~P A ~<_ ~P B ) |
| 13 |
11 12
|
mpan |
|- ( f : B -onto-> A -> ~P A ~<_ ~P B ) |
| 14 |
13
|
exlimiv |
|- ( E. f f : B -onto-> A -> ~P A ~<_ ~P B ) |
| 15 |
10 14
|
syl |
|- ( ( A ~<_ B /\ A =/= (/) ) -> ~P A ~<_ ~P B ) |
| 16 |
3
|
brrelex2i |
|- ( A ~<_ B -> B e. _V ) |
| 17 |
16
|
pwexd |
|- ( A ~<_ B -> ~P B e. _V ) |
| 18 |
|
0ss |
|- (/) C_ B |
| 19 |
18
|
sspwi |
|- ~P (/) C_ ~P B |
| 20 |
|
ssdomg |
|- ( ~P B e. _V -> ( ~P (/) C_ ~P B -> ~P (/) ~<_ ~P B ) ) |
| 21 |
17 19 20
|
mpisyl |
|- ( A ~<_ B -> ~P (/) ~<_ ~P B ) |
| 22 |
2 15 21
|
pm2.61ne |
|- ( A ~<_ B -> ~P A ~<_ ~P B ) |