Step |
Hyp |
Ref |
Expression |
1 |
|
domnsym |
|- ( A ~<_ B -> -. B ~< A ) |
2 |
|
finnum |
|- ( A e. Fin -> A e. dom card ) |
3 |
2
|
adantr |
|- ( ( A e. Fin /\ B e. V ) -> A e. dom card ) |
4 |
|
finnum |
|- ( B e. Fin -> B e. dom card ) |
5 |
|
domtri2 |
|- ( ( A e. dom card /\ B e. dom card ) -> ( A ~<_ B <-> -. B ~< A ) ) |
6 |
3 4 5
|
syl2an |
|- ( ( ( A e. Fin /\ B e. V ) /\ B e. Fin ) -> ( A ~<_ B <-> -. B ~< A ) ) |
7 |
6
|
biimprd |
|- ( ( ( A e. Fin /\ B e. V ) /\ B e. Fin ) -> ( -. B ~< A -> A ~<_ B ) ) |
8 |
|
isinffi |
|- ( ( -. B e. Fin /\ A e. Fin ) -> E. a a : A -1-1-> B ) |
9 |
8
|
ancoms |
|- ( ( A e. Fin /\ -. B e. Fin ) -> E. a a : A -1-1-> B ) |
10 |
9
|
adantlr |
|- ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> E. a a : A -1-1-> B ) |
11 |
|
brdomg |
|- ( B e. V -> ( A ~<_ B <-> E. a a : A -1-1-> B ) ) |
12 |
11
|
ad2antlr |
|- ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> ( A ~<_ B <-> E. a a : A -1-1-> B ) ) |
13 |
10 12
|
mpbird |
|- ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> A ~<_ B ) |
14 |
13
|
a1d |
|- ( ( ( A e. Fin /\ B e. V ) /\ -. B e. Fin ) -> ( -. B ~< A -> A ~<_ B ) ) |
15 |
7 14
|
pm2.61dan |
|- ( ( A e. Fin /\ B e. V ) -> ( -. B ~< A -> A ~<_ B ) ) |
16 |
1 15
|
impbid2 |
|- ( ( A e. Fin /\ B e. V ) -> ( A ~<_ B <-> -. B ~< A ) ) |