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 = Base K
opoccl.o ˙ = oc K
Assertion opococ K OP X B ˙ ˙ X = X

Proof

Step Hyp Ref Expression
1 opoccl.b B = Base K
2 opoccl.o ˙ = oc K
3 eqid K = K
4 eqid join K = join K
5 eqid meet K = meet K
6 eqid 0. K = 0. K
7 eqid 1. K = 1. K
8 1 3 2 4 5 6 7 oposlem K OP X B X B ˙ X B ˙ ˙ X = X X K X ˙ X K ˙ X X join K ˙ X = 1. K X meet K ˙ X = 0. K
9 8 3anidm23 K OP X B ˙ X B ˙ ˙ X = X X K X ˙ X K ˙ X X join K ˙ X = 1. K X meet K ˙ X = 0. K
10 9 simp1d K OP X B ˙ X B ˙ ˙ X = X X K X ˙ X K ˙ X
11 10 simp2d K OP X B ˙ ˙ X = X