Step |
Hyp |
Ref |
Expression |
1 |
|
cardid2 |
|- ( A e. dom card -> ( card ` A ) ~~ A ) |
2 |
1
|
ensymd |
|- ( A e. dom card -> A ~~ ( card ` A ) ) |
3 |
|
breq2 |
|- ( ( card ` A ) = (/) -> ( A ~~ ( card ` A ) <-> A ~~ (/) ) ) |
4 |
|
en0 |
|- ( A ~~ (/) <-> A = (/) ) |
5 |
3 4
|
bitrdi |
|- ( ( card ` A ) = (/) -> ( A ~~ ( card ` A ) <-> A = (/) ) ) |
6 |
2 5
|
syl5ibcom |
|- ( A e. dom card -> ( ( card ` A ) = (/) -> A = (/) ) ) |
7 |
|
fveq2 |
|- ( A = (/) -> ( card ` A ) = ( card ` (/) ) ) |
8 |
|
card0 |
|- ( card ` (/) ) = (/) |
9 |
7 8
|
eqtrdi |
|- ( A = (/) -> ( card ` A ) = (/) ) |
10 |
6 9
|
impbid1 |
|- ( A e. dom card -> ( ( card ` A ) = (/) <-> A = (/) ) ) |