Step |
Hyp |
Ref |
Expression |
1 |
|
sdomdom |
|- ( A ~< B -> A ~<_ B ) |
2 |
|
domtr |
|- ( ( A ~<_ B /\ B ~<_ C ) -> A ~<_ C ) |
3 |
1 2
|
sylan |
|- ( ( A ~< B /\ B ~<_ C ) -> A ~<_ C ) |
4 |
|
simpl |
|- ( ( A ~< B /\ B ~<_ C ) -> A ~< B ) |
5 |
|
simpr |
|- ( ( A ~< B /\ B ~<_ C ) -> B ~<_ C ) |
6 |
|
ensym |
|- ( A ~~ C -> C ~~ A ) |
7 |
|
domentr |
|- ( ( B ~<_ C /\ C ~~ A ) -> B ~<_ A ) |
8 |
5 6 7
|
syl2an |
|- ( ( ( A ~< B /\ B ~<_ C ) /\ A ~~ C ) -> B ~<_ A ) |
9 |
|
domnsym |
|- ( B ~<_ A -> -. A ~< B ) |
10 |
8 9
|
syl |
|- ( ( ( A ~< B /\ B ~<_ C ) /\ A ~~ C ) -> -. A ~< B ) |
11 |
10
|
ex |
|- ( ( A ~< B /\ B ~<_ C ) -> ( A ~~ C -> -. A ~< B ) ) |
12 |
4 11
|
mt2d |
|- ( ( A ~< B /\ B ~<_ C ) -> -. A ~~ C ) |
13 |
|
brsdom |
|- ( A ~< C <-> ( A ~<_ C /\ -. A ~~ C ) ) |
14 |
3 12 13
|
sylanbrc |
|- ( ( A ~< B /\ B ~<_ C ) -> A ~< C ) |