Step |
Hyp |
Ref |
Expression |
1 |
|
relsdom |
|- Rel ~< |
2 |
1
|
brrelex1i |
|- ( A ~< B -> A e. _V ) |
3 |
|
ssdif0 |
|- ( B C_ A <-> ( B \ A ) = (/) ) |
4 |
|
ssdomg |
|- ( A e. _V -> ( B C_ A -> B ~<_ A ) ) |
5 |
|
domnsym |
|- ( B ~<_ A -> -. A ~< B ) |
6 |
4 5
|
syl6 |
|- ( A e. _V -> ( B C_ A -> -. A ~< B ) ) |
7 |
3 6
|
syl5bir |
|- ( A e. _V -> ( ( B \ A ) = (/) -> -. A ~< B ) ) |
8 |
2 7
|
syl |
|- ( A ~< B -> ( ( B \ A ) = (/) -> -. A ~< B ) ) |
9 |
8
|
con2d |
|- ( A ~< B -> ( A ~< B -> -. ( B \ A ) = (/) ) ) |
10 |
9
|
pm2.43i |
|- ( A ~< B -> -. ( B \ A ) = (/) ) |
11 |
10
|
neqned |
|- ( A ~< B -> ( B \ A ) =/= (/) ) |