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

Theorem opococ 37770
Description: Double negative law for orthoposets. (ococ 30452 analog.) (Contributed by NM, 13-Sep-2011.)
Hypotheses
Ref Expression
opoccl.b 𝐵 = (Base‘𝐾)
opoccl.o = (oc‘𝐾)
Assertion
Ref Expression
opococ ((𝐾 ∈ OP ∧ 𝑋𝐵) → ( ‘( 𝑋)) = 𝑋)

Proof of Theorem opococ
StepHypRef Expression
1 opoccl.b . . . . 5 𝐵 = (Base‘𝐾)
2 eqid 2731 . . . . 5 (le‘𝐾) = (le‘𝐾)
3 opoccl.o . . . . 5 = (oc‘𝐾)
4 eqid 2731 . . . . 5 (join‘𝐾) = (join‘𝐾)
5 eqid 2731 . . . . 5 (meet‘𝐾) = (meet‘𝐾)
6 eqid 2731 . . . . 5 (0.‘𝐾) = (0.‘𝐾)
7 eqid 2731 . . . . 5 (1.‘𝐾) = (1.‘𝐾)
81, 2, 3, 4, 5, 6, 7oposlem 37757 . . . 4 ((𝐾 ∈ OP ∧ 𝑋𝐵𝑋𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))) ∧ (𝑋(join‘𝐾)( 𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( 𝑋)) = (0.‘𝐾)))
983anidm23 1421 . . 3 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))) ∧ (𝑋(join‘𝐾)( 𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( 𝑋)) = (0.‘𝐾)))
109simp1d 1142 . 2 ((𝐾 ∈ OP ∧ 𝑋𝐵) → (( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))))
1110simp2d 1143 1 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ( ‘( 𝑋)) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106   class class class wbr 5132  cfv 6523  (class class class)co 7384  Basecbs 17116  lecple 17176  occoc 17177  joincjn 18236  meetcmee 18237  0.cp0 18348  1.cp1 18349  OPcops 37747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-nul 5290
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3426  df-v 3468  df-dif 3938  df-un 3940  df-in 3942  df-ss 3952  df-nul 4310  df-if 4514  df-sn 4614  df-pr 4616  df-op 4620  df-uni 4893  df-br 5133  df-dm 5670  df-iota 6475  df-fv 6531  df-ov 7387  df-oposet 37751
This theorem is referenced by:  opcon3b  37771  opcon2b  37772  oplecon3b  37775  oplecon1b  37776  opltcon1b  37780  opltcon2b  37781  oldmm2  37793  oldmm3N  37794  oldmm4  37795  oldmj1  37796  oldmj2  37797  oldmj3  37798  oldmj4  37799  olm11  37802  omllaw4  37821  cmt2N  37825  glbconN  37952  glbconNOLD  37953  1cvratex  38049  1cvrjat  38051  polval2N  38482  2polpmapN  38489  2polvalN  38490  2polatN  38508  lhpoc2N  38591  doch2val2  39940  dochocss  39942  dochoc  39943
  Copyright terms: Public domain W3C validator