Step |
Hyp |
Ref |
Expression |
1 |
|
domnsym |
|- ( A ~<_ B -> -. B ~< A ) |
2 |
|
sdomdom |
|- ( A ~< B -> A ~<_ B ) |
3 |
2
|
con3i |
|- ( -. A ~<_ B -> -. A ~< B ) |
4 |
|
fidomtri |
|- ( ( B e. Fin /\ A e. V ) -> ( B ~<_ A <-> -. A ~< B ) ) |
5 |
4
|
ancoms |
|- ( ( A e. V /\ B e. Fin ) -> ( B ~<_ A <-> -. A ~< B ) ) |
6 |
3 5
|
syl5ibr |
|- ( ( A e. V /\ B e. Fin ) -> ( -. A ~<_ B -> B ~<_ A ) ) |
7 |
|
ensym |
|- ( B ~~ A -> A ~~ B ) |
8 |
|
endom |
|- ( A ~~ B -> A ~<_ B ) |
9 |
7 8
|
syl |
|- ( B ~~ A -> A ~<_ B ) |
10 |
9
|
con3i |
|- ( -. A ~<_ B -> -. B ~~ A ) |
11 |
6 10
|
jca2 |
|- ( ( A e. V /\ B e. Fin ) -> ( -. A ~<_ B -> ( B ~<_ A /\ -. B ~~ A ) ) ) |
12 |
|
brsdom |
|- ( B ~< A <-> ( B ~<_ A /\ -. B ~~ A ) ) |
13 |
11 12
|
syl6ibr |
|- ( ( A e. V /\ B e. Fin ) -> ( -. A ~<_ B -> B ~< A ) ) |
14 |
13
|
con1d |
|- ( ( A e. V /\ B e. Fin ) -> ( -. B ~< A -> A ~<_ B ) ) |
15 |
1 14
|
impbid2 |
|- ( ( A e. V /\ B e. Fin ) -> ( A ~<_ B <-> -. B ~< A ) ) |