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

Theorem opococ 32673
Description: Double negative law for orthoposets. (ococ 26996 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 2423 . . . . 5  |-  ( le
`  K )  =  ( le `  K
)
3 opoccl.o . . . . 5  |-  ._|_  =  ( oc `  K )
4 eqid 2423 . . . . 5  |-  ( join `  K )  =  (
join `  K )
5 eqid 2423 . . . . 5  |-  ( meet `  K )  =  (
meet `  K )
6 eqid 2423 . . . . 5  |-  ( 0.
`  K )  =  ( 0. `  K
)
7 eqid 2423 . . . . 5  |-  ( 1.
`  K )  =  ( 1. `  K
)
81, 2, 3, 4, 5, 6, 7oposlem 32660 . . . 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 1872   class class class wbr 4361   ` cfv 5539  (class class class)co 6244   Basecbs 15059   lecple 15135   occoc 15136   joincjn 16127   meetcmee 16128   0.cp0 16221   1.cp1 16222   OPcops 32650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-nul 4493
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-dm 4801  df-iota 5503  df-fv 5547  df-ov 6247  df-oposet 32654
This theorem is referenced by:  opcon3b  32674  opcon2b  32675  oplecon3b  32678  oplecon1b  32679  opltcon1b  32683  opltcon2b  32684  oldmm2  32696  oldmm3N  32697  oldmm4  32698  oldmj1  32699  oldmj2  32700  oldmj3  32701  oldmj4  32702  olm11  32705  omllaw4  32724  cmt2N  32728  glbconN  32854  1cvratex  32950  1cvrjat  32952  polval2N  33383  2polpmapN  33390  2polvalN  33391  2polatN  33409  lhpoc2N  33492  doch2val2  34844  dochocss  34846  dochoc  34847
  Copyright terms: Public domain W3C validator