Step |
Hyp |
Ref |
Expression |
1 |
|
brwdomi |
|- ( B ~<_* A -> ( B = (/) \/ E. f f : A -onto-> B ) ) |
2 |
|
simpr |
|- ( ( A e. dom card /\ B = (/) ) -> B = (/) ) |
3 |
|
0fin |
|- (/) e. Fin |
4 |
|
finnum |
|- ( (/) e. Fin -> (/) e. dom card ) |
5 |
3 4
|
ax-mp |
|- (/) e. dom card |
6 |
2 5
|
eqeltrdi |
|- ( ( A e. dom card /\ B = (/) ) -> B e. dom card ) |
7 |
|
fonum |
|- ( ( A e. dom card /\ f : A -onto-> B ) -> B e. dom card ) |
8 |
7
|
ex |
|- ( A e. dom card -> ( f : A -onto-> B -> B e. dom card ) ) |
9 |
8
|
exlimdv |
|- ( A e. dom card -> ( E. f f : A -onto-> B -> B e. dom card ) ) |
10 |
9
|
imp |
|- ( ( A e. dom card /\ E. f f : A -onto-> B ) -> B e. dom card ) |
11 |
6 10
|
jaodan |
|- ( ( A e. dom card /\ ( B = (/) \/ E. f f : A -onto-> B ) ) -> B e. dom card ) |
12 |
1 11
|
sylan2 |
|- ( ( A e. dom card /\ B ~<_* A ) -> B e. dom card ) |