Description: Contraposition law for strict ordering in orthoposets. ( chpsscon3 analog.) (Contributed by NM, 4-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opltcon3.b | |
|
opltcon3.s | |
||
opltcon3.o | |
||
Assertion | opltcon3b | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opltcon3.b | |
|
2 | opltcon3.s | |
|
3 | opltcon3.o | |
|
4 | eqid | |
|
5 | 1 4 3 | oplecon3b | |
6 | 1 4 3 | oplecon3b | |
7 | 6 | 3com23 | |
8 | 7 | notbid | |
9 | 5 8 | anbi12d | |
10 | opposet | |
|
11 | 1 4 2 | pltval3 | |
12 | 10 11 | syl3an1 | |
13 | 10 | 3ad2ant1 | |
14 | 1 3 | opoccl | |
15 | 14 | 3adant2 | |
16 | 1 3 | opoccl | |
17 | 16 | 3adant3 | |
18 | 1 4 2 | pltval3 | |
19 | 13 15 17 18 | syl3anc | |
20 | 9 12 19 | 3bitr4d | |