# Metamath Proof Explorer

## Theorem opnoncon

Description: Law of contradiction for orthoposets. ( chocin analog.) (Contributed by NM, 13-Sep-2011)

Ref Expression
Hypotheses opnoncon.b
`|- B = ( Base ` K )`
opnoncon.o
`|- ._|_ = ( oc ` K )`
opnoncon.m
`|- ./\ = ( meet ` K )`
opnoncon.z
`|- .0. = ( 0. ` K )`
Assertion opnoncon
`|- ( ( K e. OP /\ X e. B ) -> ( X ./\ ( ._|_ ` X ) ) = .0. )`

### Proof

Step Hyp Ref Expression
1 opnoncon.b
` |-  B = ( Base ` K )`
2 opnoncon.o
` |-  ._|_ = ( oc ` K )`
3 opnoncon.m
` |-  ./\ = ( meet ` K )`
4 opnoncon.z
` |-  .0. = ( 0. ` K )`
5 eqid
` |-  ( le ` K ) = ( le ` K )`
6 eqid
` |-  ( join ` K ) = ( join ` K )`
7 eqid
` |-  ( 1. ` K ) = ( 1. ` K )`
8 1 5 2 6 3 4 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 ./\ ( ._|_ ` X ) ) = .0. ) )`
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 ./\ ( ._|_ ` X ) ) = .0. ) )`
10 9 simp3d
` |-  ( ( K e. OP /\ X e. B ) -> ( X ./\ ( ._|_ ` X ) ) = .0. )`