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 36946
Description: Double negative law for orthoposets. (ococ 29487 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 2737 . . . . 5 (le‘𝐾) = (le‘𝐾)
3 opoccl.o . . . . 5 = (oc‘𝐾)
4 eqid 2737 . . . . 5 (join‘𝐾) = (join‘𝐾)
5 eqid 2737 . . . . 5 (meet‘𝐾) = (meet‘𝐾)
6 eqid 2737 . . . . 5 (0.‘𝐾) = (0.‘𝐾)
7 eqid 2737 . . . . 5 (1.‘𝐾) = (1.‘𝐾)
81, 2, 3, 4, 5, 6, 7oposlem 36933 . . . 4 ((𝐾 ∈ OP ∧ 𝑋𝐵𝑋𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))) ∧ (𝑋(join‘𝐾)( 𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( 𝑋)) = (0.‘𝐾)))
983anidm23 1423 . . 3 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))) ∧ (𝑋(join‘𝐾)( 𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( 𝑋)) = (0.‘𝐾)))
109simp1d 1144 . 2 ((𝐾 ∈ OP ∧ 𝑋𝐵) → (( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( 𝑋)(le‘𝐾)( 𝑋))))
1110simp2d 1145 1 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ( ‘( 𝑋)) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2110   class class class wbr 5053  cfv 6380  (class class class)co 7213  Basecbs 16760  lecple 16809  occoc 16810  joincjn 17818  meetcmee 17819  0.cp0 17929  1.cp1 17930  OPcops 36923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-nul 5199
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-dm 5561  df-iota 6338  df-fv 6388  df-ov 7216  df-oposet 36927
This theorem is referenced by:  opcon3b  36947  opcon2b  36948  oplecon3b  36951  oplecon1b  36952  opltcon1b  36956  opltcon2b  36957  oldmm2  36969  oldmm3N  36970  oldmm4  36971  oldmj1  36972  oldmj2  36973  oldmj3  36974  oldmj4  36975  olm11  36978  omllaw4  36997  cmt2N  37001  glbconN  37128  1cvratex  37224  1cvrjat  37226  polval2N  37657  2polpmapN  37664  2polvalN  37665  2polatN  37683  lhpoc2N  37766  doch2val2  39115  dochocss  39117  dochoc  39118
  Copyright terms: Public domain W3C validator