Metamath Proof Explorer


Theorem oplecon3b

Description: Contraposition law for orthoposets. ( chsscon3 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses opcon3.b B=BaseK
opcon3.l ˙=K
opcon3.o ˙=ocK
Assertion oplecon3b KOPXBYBX˙Y˙Y˙˙X

Proof

Step Hyp Ref Expression
1 opcon3.b B=BaseK
2 opcon3.l ˙=K
3 opcon3.o ˙=ocK
4 1 2 3 oplecon3 KOPXBYBX˙Y˙Y˙˙X
5 simp1 KOPXBYBKOP
6 1 3 opoccl KOPYB˙YB
7 6 3adant2 KOPXBYB˙YB
8 1 3 opoccl KOPXB˙XB
9 8 3adant3 KOPXBYB˙XB
10 1 2 3 oplecon3 KOP˙YB˙XB˙Y˙˙X˙˙X˙˙˙Y
11 5 7 9 10 syl3anc KOPXBYB˙Y˙˙X˙˙X˙˙˙Y
12 1 3 opococ KOPXB˙˙X=X
13 12 3adant3 KOPXBYB˙˙X=X
14 1 3 opococ KOPYB˙˙Y=Y
15 14 3adant2 KOPXBYB˙˙Y=Y
16 13 15 breq12d KOPXBYB˙˙X˙˙˙YX˙Y
17 11 16 sylibd KOPXBYB˙Y˙˙XX˙Y
18 4 17 impbid KOPXBYBX˙Y˙Y˙˙X