# Metamath Proof Explorer

## Theorem opexmid

Description: Law of excluded middle for orthoposets. ( chjo analog.) (Contributed by NM, 13-Sep-2011)

Ref Expression
Hypotheses opexmid.b
`|- B = ( Base ` K )`
opexmid.o
`|- ._|_ = ( oc ` K )`
opexmid.j
`|- .\/ = ( join ` K )`
opexmid.u
`|- .1. = ( 1. ` K )`
Assertion opexmid
`|- ( ( K e. OP /\ X e. B ) -> ( X .\/ ( ._|_ ` X ) ) = .1. )`

### Proof

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