# 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 e. OP /\ X e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )`

### Proof

Step Hyp Ref Expression
1 opoccl.b
` |-  B = ( Base ` K )`
2 opoccl.o
` |-  ._|_ = ( oc ` K )`
3 eqid
` |-  ( le ` K ) = ( le ` 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 e. OP /\ X e. B /\ X e. B ) -> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X ( le ` K ) X -> ( ._|_ ` X ) ( le ` K ) ( ._|_ ` X ) ) ) /\ ( X ( join ` K ) ( ._|_ ` X ) ) = ( 1. ` K ) /\ ( X ( meet ` K ) ( ._|_ ` X ) ) = ( 0. ` K ) ) )`
9 8 3anidm23
` |-  ( ( K e. OP /\ X e. B ) -> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X ( le ` K ) X -> ( ._|_ ` X ) ( le ` K ) ( ._|_ ` X ) ) ) /\ ( X ( join ` K ) ( ._|_ ` X ) ) = ( 1. ` K ) /\ ( X ( meet ` K ) ( ._|_ ` X ) ) = ( 0. ` K ) ) )`
10 9 simp1d
` |-  ( ( K e. OP /\ X e. B ) -> ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X ( le ` K ) X -> ( ._|_ ` X ) ( le ` K ) ( ._|_ ` X ) ) ) )`
11 10 simp2d
` |-  ( ( K e. OP /\ X e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )`