Step |
Hyp |
Ref |
Expression |
1 |
|
carddom2 |
|- ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) C_ ( card ` B ) <-> A ~<_ B ) ) |
2 |
|
cardon |
|- ( card ` A ) e. On |
3 |
|
cardon |
|- ( card ` B ) e. On |
4 |
|
ontri1 |
|- ( ( ( card ` A ) e. On /\ ( card ` B ) e. On ) -> ( ( card ` A ) C_ ( card ` B ) <-> -. ( card ` B ) e. ( card ` A ) ) ) |
5 |
2 3 4
|
mp2an |
|- ( ( card ` A ) C_ ( card ` B ) <-> -. ( card ` B ) e. ( card ` A ) ) |
6 |
|
cardsdom2 |
|- ( ( B e. dom card /\ A e. dom card ) -> ( ( card ` B ) e. ( card ` A ) <-> B ~< A ) ) |
7 |
6
|
ancoms |
|- ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` B ) e. ( card ` A ) <-> B ~< A ) ) |
8 |
7
|
notbid |
|- ( ( A e. dom card /\ B e. dom card ) -> ( -. ( card ` B ) e. ( card ` A ) <-> -. B ~< A ) ) |
9 |
5 8
|
syl5bb |
|- ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) C_ ( card ` B ) <-> -. B ~< A ) ) |
10 |
1 9
|
bitr3d |
|- ( ( A e. dom card /\ B e. dom card ) -> ( A ~<_ B <-> -. B ~< A ) ) |