Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  opococ Structured version   Unicode version

Theorem opococ 32470
Description: Double negative law for orthoposets. (ococ 26894 analog.) (Contributed by NM, 13-Sep-2011.)
Hypotheses
Ref Expression
opoccl.b  |-  B  =  ( Base `  K
)
opoccl.o  |-  ._|_  =  ( oc `  K )
Assertion
Ref Expression
opococ  |-  ( ( K  e.  OP  /\  X  e.  B )  ->  (  ._|_  `  (  ._|_  `  X ) )  =  X )

Proof of Theorem opococ
StepHypRef Expression
1 opoccl.b . . . . 5  |-  B  =  ( Base `  K
)
2 eqid 2429 . . . . 5  |-  ( le
`  K )  =  ( le `  K
)
3 opoccl.o . . . . 5  |-  ._|_  =  ( oc `  K )
4 eqid 2429 . . . . 5  |-  ( join `  K )  =  (
join `  K )
5 eqid 2429 . . . . 5  |-  ( meet `  K )  =  (
meet `  K )
6 eqid 2429 . . . . 5  |-  ( 0.
`  K )  =  ( 0. `  K
)
7 eqid 2429 . . . . 5  |-  ( 1.
`  K )  =  ( 1. `  K
)
81, 2, 3, 4, 5, 6, 7oposlem 32457 . . . 4  |-  ( ( 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 ) ) )
983anidm23 1323 . . 3  |-  ( ( 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 ) ) )
109simp1d 1017 . 2  |-  ( ( K  e.  OP  /\  X  e.  B )  ->  ( (  ._|_  `  X
)  e.  B  /\  (  ._|_  `  (  ._|_  `  X ) )  =  X  /\  ( X ( le `  K
) X  ->  (  ._|_  `  X ) ( le `  K ) (  ._|_  `  X ) ) ) )
1110simp2d 1018 1  |-  ( ( K  e.  OP  /\  X  e.  B )  ->  (  ._|_  `  (  ._|_  `  X ) )  =  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1870   class class class wbr 4426   ` cfv 5601  (class class class)co 6305   Basecbs 15084   lecple 15159   occoc 15160   joincjn 16140   meetcmee 16141   0.cp0 16234   1.cp1 16235   OPcops 32447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-dm 4864  df-iota 5565  df-fv 5609  df-ov 6308  df-oposet 32451
This theorem is referenced by:  opcon3b  32471  opcon2b  32472  oplecon3b  32475  oplecon1b  32476  opltcon1b  32480  opltcon2b  32481  oldmm2  32493  oldmm3N  32494  oldmm4  32495  oldmj1  32496  oldmj2  32497  oldmj3  32498  oldmj4  32499  olm11  32502  omllaw4  32521  cmt2N  32525  glbconN  32651  1cvratex  32747  1cvrjat  32749  polval2N  33180  2polpmapN  33187  2polvalN  33188  2polatN  33206  lhpoc2N  33289  doch2val2  34641  dochocss  34643  dochoc  34644
  Copyright terms: Public domain W3C validator