Metamath Proof Explorer


Theorem opococ

Description: Double negative law for orthoposets. ( ococ analog.) (Contributed by NM, 13-Sep-2011)

Ref Expression
Hypotheses opoccl.b B=BaseK
opoccl.o ˙=ocK
Assertion opococ KOPXB˙˙X=X

Proof

Step Hyp Ref Expression
1 opoccl.b B=BaseK
2 opoccl.o ˙=ocK
3 eqid K=K
4 eqid joinK=joinK
5 eqid meetK=meetK
6 eqid 0.K=0.K
7 eqid 1.K=1.K
8 1 3 2 4 5 6 7 oposlem KOPXBXB˙XB˙˙X=XXKX˙XK˙XXjoinK˙X=1.KXmeetK˙X=0.K
9 8 3anidm23 KOPXB˙XB˙˙X=XXKX˙XK˙XXjoinK˙X=1.KXmeetK˙X=0.K
10 9 simp1d KOPXB˙XB˙˙X=XXKX˙XK˙X
11 10 simp2d KOPXB˙˙X=X