Metamath Proof Explorer


Theorem opltcon3b

Description: Contraposition law for strict ordering in orthoposets. ( chpsscon3 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses opltcon3.b B=BaseK
opltcon3.s <˙=<K
opltcon3.o ˙=ocK
Assertion opltcon3b KOPXBYBX<˙Y˙Y<˙˙X

Proof

Step Hyp Ref Expression
1 opltcon3.b B=BaseK
2 opltcon3.s <˙=<K
3 opltcon3.o ˙=ocK
4 eqid K=K
5 1 4 3 oplecon3b KOPXBYBXKY˙YK˙X
6 1 4 3 oplecon3b KOPYBXBYKX˙XK˙Y
7 6 3com23 KOPXBYBYKX˙XK˙Y
8 7 notbid KOPXBYB¬YKX¬˙XK˙Y
9 5 8 anbi12d KOPXBYBXKY¬YKX˙YK˙X¬˙XK˙Y
10 opposet KOPKPoset
11 1 4 2 pltval3 KPosetXBYBX<˙YXKY¬YKX
12 10 11 syl3an1 KOPXBYBX<˙YXKY¬YKX
13 10 3ad2ant1 KOPXBYBKPoset
14 1 3 opoccl KOPYB˙YB
15 14 3adant2 KOPXBYB˙YB
16 1 3 opoccl KOPXB˙XB
17 16 3adant3 KOPXBYB˙XB
18 1 4 2 pltval3 KPoset˙YB˙XB˙Y<˙˙X˙YK˙X¬˙XK˙Y
19 13 15 17 18 syl3anc KOPXBYB˙Y<˙˙X˙YK˙X¬˙XK˙Y
20 9 12 19 3bitr4d KOPXBYBX<˙Y˙Y<˙˙X